∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso]
  [P.RespectsLeft AlgebraicGeometry.IsOpenImmersion],
  AlgebraicGeometry.IsZariskiLocalAtSource (AlgebraicGeometry.sourceLocalClosure AlgebraicGeometry.IsOpenImmersion P)