theorem PiBase.instHasCountableKNetworkOfAlephZeroSpace {X : Type u} [TopologicalSpace X] [AlephZeroSpace X] : HasCountableKNetwork X

Theorem T116: P179 (AlephZeroSpace) => P183 (HasCountableKNetwork)

theorem PiBase.Formal.T116 : P179 ≤ P183