instance PiBase.instFunctionallyT2SpaceOfTotallySeparatedSpace {X : Type u} [TopologicalSpace X] [h : TotallySeparatedSpace X] : FunctionallyT2Space X

Theorem T48: P48 (TotallySeparatedSpace) => P9 (FunctionallyT2Space)

theorem PiBase.Formal.T48 : P48 ≤ P9