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

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

hence
not Tdisk ((0. (TOP-REAL n)),1) is without_boundary
; :: thesis: verum
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;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