∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {j : I} (Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)),
  (∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)) →
    (∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty) →
      (∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)) →
        (∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j),
            Set.MapsTo (⇑(D.map hi'i)) (Z i' (CategoryTheory.CategoryStruct.comp hi'i hij)) (Z i hij)) →
          ∃ s, ∀ (i : I) (hij : i ⟶ j), (c.π.app i) s ∈ Z i hij