instance PiBase.instCountableOfAnticompactSpaceOfSigmaCompactSpace {X : Type u} [TopologicalSpace X] [h : AnticompactSpace X] [h' : SigmaCompactSpace X] : Countable X

Theorem T304: P136 (AnticompactSpace) + P17 (SigmaCompactSpace) => P57 (Countable)

theorem PiBase.Formal.T304 : P136 ⊓ P17 ≤ P57