instance PiBase.instLocallyNEuclideanSpaceOfLocallyOneEuclideanSpace {X : Type u} [TopologicalSpace X] [h : LocallyOneEuclideanSpace X] : LocallyNEuclideanSpace X

Theorem T759: P155 (LocallyOneEuclideanSpace) => P123 (LocallyNEuclideanSpace)

theorem PiBase.Formal.T759 : P155 ≤ P123