instance PiBase.instLocallyFiniteSpaceOfFinite {X : Type u} [TopologicalSpace X] [h : Finite X] : LocallyFiniteSpace X

Theorem T266: P78 (Finite) => P94 (LocallyFiniteSpace)

theorem PiBase.Formal.T266 : P78 ≤ P94