instance PiBase.instMetaLindelofSpaceOfParaLindelofSpace {X : Type u} [TopologicalSpace X] [h : ParaLindelofSpace X] : MetaLindelofSpace X

Theorem T655: P105 (ParaLindelofSpace) => P83 (MetaLindelofSpace)

theorem PiBase.Formal.T655 : P105 ≤ P83