set TR = TOP-REAL n;
set S = Sphere ((0. (TOP-REAL n)),1);
let M be non empty n -locally_euclidean TopSpace; :: thesis: M is without_boundary
assume M is with_boundary ; :: thesis: contradiction
then consider p being object such that
A1: p in Fr M by XBOOLE_0:def 1;
reconsider p = p as Point of M by A1;
consider U being a_neighborhood of p, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that
A2: h is being_homeomorphism and
A3: h . p in Sphere ((0. (TOP-REAL m)),1) by A1, Th5;
A4: p in Int U by CONNSP_2:def 1;
consider W being a_neighborhood of p such that
A5: M | W, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;
A6: p in Int W by CONNSP_2:def 1;
M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A2, T_0TOPSP:def 1;
then reconsider hp = h . p as Point of (TOP-REAL n) by A3, A6, A4, XBOOLE_0:3, BROUWER3:14, A5;
hp = 0. (TOP-REAL n) by A3;
then |.(0. (TOP-REAL n)).| = 1 by A3, TOPREAL9:12;
hence contradiction ; :: thesis: verum