instance PiBase.instPerfectlyNormalSpaceOfNormalSpaceOfGδSpace {X : Type u} [TopologicalSpace X] [NormalSpace X] [h' : GδSpace X] : PerfectlyNormalSpace X

Theorem T257: P13 (NormalSpace) + P132 (GδSpace) => P15 (PerfectlyNormalSpace)

theorem PiBase.Formal.T257 : P13 ⊓ P132 ≤ P15