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

Theorem T117: P183 (HasCountableKNetwork) + P5 (T3Space) => P179 (AlephZeroSpace)

theorem PiBase.Formal.T117 : P183 ⊓ P5 ≤ P179