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

Theorem T649: P126 (DoorSpace) + P137ᶜ (Nonempty) => P107 (HasClosedPoint)

theorem PiBase.Formal.T649 : P126 ⊓ P137ᶜ ≤ P107