∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V → ∀ x ∈ U ⊓ V, ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f