theorem PiBase.instNormalSpaceOfCompletelyNormalSpace {X : Type u} [TopologicalSpace X] [CompletelyNormalSpace X] : NormalSpace X

Theorem T36: P14 (CompletelyNormalSpace) => P13 (NormalSpace)

theorem PiBase.Formal.T36 : P14 ≤ P13