theorem PiBase.instNotTotallyPathDisconnectedSpaceOfPrepathConnectedSpaceOfNontrivial {X : Type u} [TopologicalSpace X] [h : PrepathConnectedSpace X] [h' : Nontrivial X] : ¬TotallyPathDisconnectedSpace X

Theorem T88: P37 (PrepathConnectedSpace) + P125 (Nontrivial) => P46 (¬TotallyPathDisconnectedSpace)

theorem PiBase.Formal.T88 : P37 ⊓ P125 ≤ P46ᶜ