instance PiBase.instMengerSpaceOfRothbergerSpace {X : Type u} [TopologicalSpace X] [h : RothbergerSpace X] : MengerSpace X

Theorem T160: P68 (RothbergerSpace) => P66 (MengerSpace)

theorem PiBase.Formal.T160 : P68 ≤ P66