instance PiBase.instMengerSpaceOfOmegaMengerSpace {X : Type u} [TopologicalSpace X] [h : OmegaMengerSpace X] : MengerSpace X

Theorem T362: P153 (OmegaMengerSpace) => P66 (MengerSpace)

theorem PiBase.Formal.T362 : P153 ≤ P66