instance PiBase.instCountableOfHasCountableExtentOfDiscreteTopology {X : Type u} [TopologicalSpace X] [h : HasCountableExtent X] [h' : DiscreteTopology X] : Countable X

Theorem T559: P198 (HasCountableExtent) + P52 (DiscreteTopology) => P57 (Countable)

theorem PiBase.Formal.T559 : P198 ⊓ P52 ≤ P57