instance PiBase.instTotallyDisconnectedSpaceOfT1SpaceOfScatteredSpace {X : Type u} [TopologicalSpace X] [T1Space X] [h : ScatteredSpace X] : TotallyDisconnectedSpace X

Theorem T43: P2 (T1Space) + P51 (ScatteredSpace) => P47 (TotallyDisconnectedSpace)

theorem PiBase.Formal.T43 : P2 ⊓ P51 ≤ P47