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