instance PiBase.instStronglyParacompactSpaceOfCompactSpace {X : Type u} [TopologicalSpace X] [h : CompactSpace X] : StronglyParacompactSpace X

Theorem T13: P16 (CompactSpace) => P145 (StronglyParacompactSpace)

theorem PiBase.Formal.T13 : P16 ≤ P145