theorem PiBase.not_CardLtContinuumOfHasClosedDiscreteSubsetCardContinuum {X : Type u} [TopologicalSpace X] [h : HasClosedDiscreteSubsetCardContinuum X] : ¬CardLtContinuum X

Theorem T834: P227 (HasClosedDiscreteSubsetCardContinuum) => P58 (¬CardLtContinuum)

theorem PiBase.Formal.T834 : P227 ≤ P58ᶜ