instance PiBase.instPseudonormalSpaceOfNormalSpace {X : Type u} [TopologicalSpace X] [h : NormalSpace X] : PseudonormalSpace X

Theorem T401: P13 (NormalSpace) => P165 (PseudonormalSpace)

theorem PiBase.Formal.T401 : P13 ≤ P165