instance PiBase.instNormalSpaceOfPseudonormalSpaceOfCountable {X : Type u} [TopologicalSpace X] [h : PseudonormalSpace X] [h' : Countable X] : NormalSpace X

Theorem T406: P165 (PseudonormalSpace) + P57 (Countable) => P13 (NormalSpace)

theorem PiBase.Formal.T406 : P165 ⊓ P57 ≤ P13