instance PiBase.instUltranormalSpaceOfUltraconnectedSpace {X : Type u} [TopologicalSpace X] [h : UltraconnectedSpace X] : UltranormalSpace X

Theorem T87: P40 (UltraconnectedSpace) => P218 (UltranormalSpace)

theorem PiBase.Formal.T87 : P40 ≤ P218