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

Theorem T338: P67 (T6Space) => P15 (PerfectlyNormalSpace)

theorem PiBase.Formal.T338 : P67 ≤ P15