theorem PiBase.not_HasACutPointOfHereditarilyConnected {X : Type u} [TopologicalSpace X] [h : HereditarilyConnected X] : ¬HasACutPoint X

Theorem T620: P196 (HereditarilyConnected) => P204 (¬HasACutPoint)

theorem PiBase.Formal.T620 : P196 ≤ P204ᶜ