theorem PiBase.instLocallyNEuclideanSpaceOfTopologicalNManifold {X : Type u} [TopologicalSpace X] [TopologicalNManifold X] : LocallyNEuclideanSpace X

Theorem T25: P124 (TopologicalNManifold) => P123 (LocallyNEuclideanSpace)

theorem PiBase.Formal.T25 : P124 ≤ P123