theorem PiBase.instAlephSpaceOfHasSigmaLocallyFiniteKNetworkOfT3Space {X : Type u} [TopologicalSpace X] [HasSigmaLocallyFiniteKNetwork X] [T3Space X] : AlephSpace X

Theorem T197: P118 (HasSigmaLocallyFiniteKNetwork) + P5 (T3Space) => P178 (AlephSpace)

theorem PiBase.Formal.T197 : P118 ⊓ P5 ≤ P178