∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presheaf.IsSheaf J P → ∀ {X : C}, ∀ S ∈ J X, CategoryTheory.Presieve.IsSheafFor P S.arrows