∀ {X Y T : AlgebraicGeometry.Scheme} {g : Y ⟶ X} {iY : Y ⟶ T} {UT : T.Opens} {UX : X.Opens} {UY : Y.Opens},
  UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT →
    UY ≤ (TopologicalSpace.Opens.map iY.base).obj UT