∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (E : CategoryTheory.PreZeroHypercover X),
  (E.presieve₀ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X) =
    ((∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (E.f i).base)) ∧ ∀ (i : E.I₀), P (E.f i))