∀ (P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative] ⦃X : Q.Over ⊤ S⦄ (S_1 : CategoryTheory.Presieve X)
  (Ti : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → S_1 f → CategoryTheory.Presieve Y),
  (S_1 ∈ fun R => ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h) →
    (∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : S_1 f),
        Ti f H ∈ fun R => ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h) →
      S_1.bind Ti ∈ fun R => ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h