instance PiBase.instMetaLindelofSpaceOfMetacompactSpace {X : Type u} [TopologicalSpace X] [h : MetacompactSpace X] : MetaLindelofSpace X

Theorem T586: P31 (MetacompactSpace) => P83 (MetaLindelofSpace)

theorem PiBase.Formal.T586 : P31 ≤ P83