True ↔ ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)), IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}