instance PiBase.instLocallyEuclideanSpaceOfLocallyNEuclideanSpace {X : Type u} [TopologicalSpace X] [h : LocallyNEuclideanSpace X] : LocallyEuclideanSpace X

Theorem T535: P123 (LocallyNEuclideanSpace) => P122 (LocallyEuclideanSpace)

theorem PiBase.Formal.T535 : P123 ≤ P122