instance PiBase.instHasCountableKNetworkOfAnticompactSpaceOfCountable {X : Type u} [TopologicalSpace X] [h : AnticompactSpace X] [Countable X] : HasCountableKNetwork X

Theorem T22: P136 (AnticompactSpace) + P57 (Countable) => P183 (HasCountableKNetwork)

theorem PiBase.Formal.T22 : P136 ⊓ P57 ≤ P183