∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative],
  AlgebraicGeometry.Scheme.pretopology P = AlgebraicGeometry.Scheme.jointlySurjectivePretopology ⊓ P.pretopology