∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (X : C)
  (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
  S ∈ {R | CategoryTheory.Sieve.generate R ∈ J X} →
    (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | CategoryTheory.Sieve.generate R ∈ J Y}) →
      S.bind Ti ∈ {R | CategoryTheory.Sieve.generate R ∈ J X}