∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : Cᵒᵖ}
  (f : X ⟶ Y) (S : { S // J₁.IsClosed S }), J₁.IsClosed (CategoryTheory.Sieve.pullback f.unop ↑S)