theorem PiBase.instSigmaCompactSpaceOfCompactSpace {X : Type u} [TopologicalSpace X] [CompactSpace X] : SigmaCompactSpace X

Theorem T121: P16 (CompactSpace) => P17 (SigmaCompactSpace)

theorem PiBase.Formal.T121 : P16 ≤ P17