instance PiBase.instLocallyCountableSpaceOfLocallyFiniteSpace {X : Type u} [TopologicalSpace X] [h : LocallyFiniteSpace X] : LocallyCountableSpace X

Theorem T564: P94 (LocallyFiniteSpace) => P93 (LocallyCountableSpace)

theorem PiBase.Formal.T564 : P94 ≤ P93