set TR = TOP-REAL n;
set S = Sphere ((0. (TOP-REAL n)),1);
let M be non empty n -locally_euclidean TopSpace; M is without_boundary
assume
M is with_boundary
; 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
; verum