instance PiBase.instTotallyPathDisconnectedSpaceOfTotallyDisconnectedSpace {X : Type u} [TopologicalSpace X] [h : TotallyDisconnectedSpace X] : TotallyPathDisconnectedSpace X

Theorem T47: P47 (TotallyDisconnectedSpace) => P46 (TotallyPathDisconnectedSpace)

theorem PiBase.Formal.T47 : P47 ≤ P46