instance PiBase.instHasACutPointOfCutPointSpace {X : Type u} [TopologicalSpace X] [h : CutPointSpace X] : HasACutPoint X

Theorem T635: P205 (CutPointSpace) => P204 (HasACutPoint)

theorem PiBase.Formal.T635 : P205 ≤ P204