instance PiBase.instRothbergerSpaceOfOmegaRothberger {X : Type u} [TopologicalSpace X] [h : OmegaRothberger X] : RothbergerSpace X

Theorem T361: P150 (OmegaRothberger) => P68 (RothbergerSpace)

theorem PiBase.Formal.T361 : P150 ≤ P68