instance PiBase.instHasCountableNetworkOfHasCountableKNetwork {X : Type u} [TopologicalSpace X] [h : HasCountableKNetwork X] : HasCountableNetwork X

Theorem T11: P183 (HasCountableKNetwork) => P182 (HasCountableNetwork)

theorem PiBase.Formal.T11 : P183 ≤ P182