instance PiBase.instHasClosedPointOfT1SpaceOfNonempty {X : Type u} [TopologicalSpace X] [h : T1Space X] [h' : Nonempty X] : HasClosedPoint X

Theorem T630: P2 (T1Space) + P137ᶜ (Nonempty) => P107 (HasClosedPoint)

theorem PiBase.Formal.T630 : P2 ⊓ P137ᶜ ≤ P107