∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v)))
  (J : CategoryTheory.GrothendieckTopology C),
  (∀ P ∈ Ps, CategoryTheory.Presieve.IsSheaf J P) → J ≤ CategoryTheory.Sheaf.finestTopology Ps