instance PiBase.instParaLindelofSpaceOfLindelofSpace {X : Type u} [TopologicalSpace X] [h : LindelofSpace X] : ParaLindelofSpace X

Theorem T654: P18 (LindelofSpace) => P105 (ParaLindelofSpace)

theorem PiBase.Formal.T654 : P18 ≤ P105