instance PiBase.instT1SpaceOfTotallyPathDisconnectedSpace {X : Type u} [TopologicalSpace X] [h : TotallyPathDisconnectedSpace X] : T1Space X

Theorem T49: P46 (TotallyPathDisconnectedSpace) => P2 (T1Space)

theorem PiBase.Formal.T49 : P46 ≤ P2