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

proof

assume A8: Tdisk ((0. (TOP-REAL n)),1) is without_boundary ; :: thesis: contradiction
Fr (Tdisk ((0. (TOP-REAL n)),1)) = the carrier of (Tdisk ((0. (TOP-REAL n)),1)) \ the carrier of (Tdisk ((0. (TOP-REAL n)),1)) by A8, SUBSET_1:def 4
.= {} by XBOOLE_1:37 ;
hence contradiction by A3, A6, A7, A5, Th5; :: thesis: verum

end;

hence not Tdisk ((0. (TOP-REAL n)),1) is without_boundary ; :: thesis: verum