class PiBase.HasClosedPoint (X : Type u_1) [TopologicalSpace X] : Prop

• has_closed_point : ∃ (x : X), IsClosed {x}