instance PiBase.instSigmaCompactSpaceOfCountable {X : Type u} [TopologicalSpace X] [h : Countable X] : SigmaCompactSpace X

Theorem T74: P57 (Countable) => P17 (SigmaCompactSpace)

theorem PiBase.Formal.T74 : P57 ≤ P17