https://www.glc.us.es/~jalonso/calculemus/15-mar-24/
f[s] ⊆ u ↔ s ⊆ f⁻¹[u]