instance PiBase.instParaLindelofSpaceOfParacompactSpace {X : Type u} [TopologicalSpace X] [h : ParacompactSpace X] : ParaLindelofSpace X

Theorem T653: P30 (ParacompactSpace) => P105 (ParaLindelofSpace)

theorem PiBase.Formal.T653 : P30 ≤ P105