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

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