theorem PiBase.instCompletelyNormalSpaceOfT5Space {X : Type u} [TopologicalSpace X] [T5Space X] : CompletelyNormalSpace X

Theorem T336: P8 (T5Space) => P14 (CompletelyNormalSpace)

theorem PiBase.Formal.T336 : P8 ≤ P14