no goals
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S : Sieve X✝
R : Presieve X✝
J J₂ : GrothendieckTopology C
X : C
⊢ ∀ (S : Sieve X), S ∈ GrothendieckTopology.sieves ⊥ X → IsSheafFor P S.arrows
simp [isSheafFor_top_sieve]