instance PiBase.instNormalSpaceOfUltranormalSpace {X : Type u} [TopologicalSpace X] [h : UltranormalSpace X] : NormalSpace X

Theorem T765: P218 (UltranormalSpace) => P13 (NormalSpace)

theorem PiBase.Formal.T765 : P218 ≤ P13