let n be Nat; :: thesis: not cl_Ball ((0. (TOP-REAL n)),1) is boundary
set TR = TOP-REAL n;
reconsider tr = TOP-REAL n as TopStruct ;
reconsider cB = cl_Ball ((0. (TOP-REAL n)),1) as Subset of tr ;
Ball ((0. (TOP-REAL n)),1) c= Int cB by TOPREAL9:16, TOPS_1:24;
hence not cl_Ball ((0. (TOP-REAL n)),1) is boundary ; :: thesis: verum