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

Theorem T182: P178 (AlephSpace) => P118 (HasSigmaLocallyFiniteKNetwork)

theorem PiBase.Formal.T182 : P178 ≤ P118