set TR = TOP-REAL n;
set M = Tdisk ((0. (TOP-REAL n)),1);
reconsider CM = [#] (Tdisk ((0. (TOP-REAL n)),1)) as non empty Subset of (Tdisk ((0. (TOP-REAL n)),1)) ;
consider p being object such that
A1:
p in Sphere ((0. (TOP-REAL n)),1)
by XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL n) by A1;
A2:
[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
Sphere ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1)
by TOPREAL9:17;
then reconsider pp = p as Point of (Tdisk ((0. (TOP-REAL n)),1)) by A2, A1;
A3:
Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1)
by BROUWER2:5;
[#] ((Tdisk ((0. (TOP-REAL n)),1)) | CM) = CM
by PRE_TOPC:def 5;
then reconsider cm = CM as non empty Subset of ((Tdisk ((0. (TOP-REAL n)),1)) | CM) ;
Int ([#] (Tdisk ((0. (TOP-REAL n)),1))) = [#] (Tdisk ((0. (TOP-REAL n)),1))
by TOPS_1:15;
then reconsider CM = CM as non empty a_neighborhood of pp by CONNSP_2:def 1;
A4:
(Tdisk ((0. (TOP-REAL n)),1)) | CM = Tdisk ((0. (TOP-REAL n)),1)
by TSEP_1:3;
Ball ((0. (TOP-REAL n)),1) c= Int (cl_Ball ((0. (TOP-REAL n)),1))
by TOPREAL9:16, TOPS_1:24;
then
( not cl_Ball ((0. (TOP-REAL n)),1) is boundary & cl_Ball ((0. (TOP-REAL n)),1) is compact )
;
then consider h being Function of ((Tdisk ((0. (TOP-REAL n)),1)) | CM),(Tdisk ((0. (TOP-REAL n)),1)) such that
A5:
h is being_homeomorphism
and
A6:
h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr (cl_Ball ((0. (TOP-REAL n)),1))
by BROUWER2:7, A4;
dom h = [#] (Tdisk ((0. (TOP-REAL n)),1))
by A5, A4, TOPS_2:def 5;
then A7:
h . pp in h .: (Sphere ((0. (TOP-REAL n)),1))
by A1, FUNCT_1:def 6;
Tdisk ((0. (TOP-REAL n)),1) is with_boundary
hence
not Tdisk ((0. (TOP-REAL n)),1) is without_boundary
; verum