instance PiBase.instMetaLindelofSpaceOfLindelofSpace {X : Type u} [TopologicalSpace X] [h : LindelofSpace X] : MetaLindelofSpace X

Theorem T587: P18 (LindelofSpace) => P83 (MetaLindelofSpace)

theorem PiBase.Formal.T587 : P18 ≤ P83