instance PiBase.instNonemptyOfHasClosedPoint {X : Type u} [TopologicalSpace X] [h : HasClosedPoint X] : Nonempty X

Theorem T621: P107 (HasClosedPoint) => P137 (¬IsEmpty)

theorem PiBase.Formal.T621 : P107 ≤ P137ᶜ