instance PiBase.instOmegaMengerSpaceOfOmegaRothberger {X : Type u} [TopologicalSpace X] [h : OmegaRothberger X] : OmegaMengerSpace X

Theorem T359: P150 (OmegaRothberger) => P153 (OmegaMengerSpace)

theorem PiBase.Formal.T359 : P150 ≤ P153