instance PiBase.instGδSpaceOfPerfectlyNormalSpace {X : Type u} [TopologicalSpace X] [h : PerfectlyNormalSpace X] : GδSpace X

Theorem T256: P15 (PerfectlyNormalSpace) => P132 (GδSpace)

theorem PiBase.Formal.T256 : P15 ≤ P132