instance PiBase.instHasSigmaLocallyFiniteNetworkOfHasSigmaLocallyFiniteKNetwork {X : Type u} [TopologicalSpace X] [h : HasSigmaLocallyFiniteKNetwork X] : HasSigmaLocallyFiniteNetwork X

Theorem T34: P118 (HasSigmaLocallyFiniteKNetwork) => P117 (HasSigmaLocallyFiniteNetwork)

theorem PiBase.Formal.T34 : P118 ≤ P117