∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [P.IsStableUnderBaseChange],
  (AlgebraicGeometry.sourceLocalClosure W P).IsStableUnderBaseChange