theorem PiBase.instT6SpaceOfT1SpaceOfPerfectlyNormalSpace {X : Type u} [TopologicalSpace X] [T1Space X] [PerfectlyNormalSpace X] : T6Space X

Theorem T153: P2 (T1Space) + P15 (PerfectlyNormalSpace) => P67 (T6Space)

theorem PiBase.Formal.T153 : P2 ⊓ P15 ≤ P67