theorem PiBase.instNormalSpaceOfT4Space {X : Type u} [TopologicalSpace X] [T4Space X] : NormalSpace X

Theorem T335: P7 (T4Space) => P13 (NormalSpace)

theorem PiBase.Formal.T335 : P7 ≤ P13