let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let p be Point of (TOP-REAL n); :: thesis: for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let r be real number ; :: thesis: ( r > 0 implies Fr (cl_Ball (p,r)) = Sphere (p,r) )
set TR = TOP-REAL n;
assume A1: r > 0 ; :: thesis: Fr (cl_Ball (p,r)) = Sphere (p,r)
set CB = cl_Ball (p,r);
set B = Ball (p,r);
set S = Sphere (p,r);
reconsider tr = TOP-REAL n as TopSpace ;
reconsider cb = cl_Ball (p,r) as Subset of tr ;
A2: n in NAT by ORDINAL1:def 12;
then A3: Ball (p,r) misses Sphere (p,r) by TOPREAL9:19;
A4: (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) by A2, TOPREAL9:18;
A5: Int cb c= Ball (p,r)

proof

reconsider ONE = 1 as Real ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Int cb or x in Ball (p,r) )
assume x in Int cb ; :: thesis: x in Ball (p,r)
then consider Q being Subset of (TOP-REAL n) such that
A6: Q is open and
A7: Q c= cl_Ball (p,r) and
A8: x in Q by TOPS_1:22;
reconsider q = x as Point of (TOP-REAL n) by A8;
consider w being real positive number such that
A9: Ball (q,w) c= Q by A6, A8, TOPS_4:2;
assume not x in Ball (p,r) ; :: thesis: contradiction
then q in Sphere (p,r) by A4, A7, A8, XBOOLE_0:def 3;
then A10: |.(q - p).| = r by A2, TOPREAL9:9;
set w2 = w / 2;
set wr = ((w / 2) / r) * (q - p);
A11: abs ((w / 2) / r) = (w / 2) / r by A1, ABSVALUE:def 1;
A12: ((((w / 2) / r) * (q - p)) + q) - p = (((w / 2) / r) * (q - p)) + (q - p) by RLVECT_1:28
.= (((w / 2) / r) * (q - p)) + (ONE * (q - p)) by RLVECT_1:def 8
.= (((w / 2) / r) + ONE) * (q - p) by RLVECT_1:def 6 ;
|.(((((w / 2) / r) * (q - p)) + q) - q).| = |.((((w / 2) / r) * (q - p)) + (q - q)).| by EUCLID:45
.= |.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).| by RLVECT_1:15
.= |.(((w / 2) / r) * (q - p)).| by RLVECT_1:def 4
.= ((w / 2) / r) * r by A2, A10, A11, TOPRNS_1:7
.= w / 2 by A1, XCMPLX_1:87 ;
then |.(((((w / 2) / r) * (q - p)) + q) - q).| < w by XREAL_1:216;
then (((w / 2) / r) * (q - p)) + q in Ball (q,w) ;
then A13: (((w / 2) / r) * (q - p)) + q in Q by A9;
A14: ((w / 2) / r) + ONE = ((w / 2) / r) + (r / r) by A1, XCMPLX_1:60
.= ((w / 2) + r) / r ;
A15: (w / 2) + r > 0 + r by XREAL_1:6;
abs (((w / 2) + r) / r) = ((w / 2) + r) / r by A1, ABSVALUE:def 1;
then |.(((((w / 2) / r) * (q - p)) + q) - p).| = (((w / 2) + r) / r) * r by A2, A10, A14, A12, TOPRNS_1:7
.= (w / 2) + r by A1, XCMPLX_1:87 ;
hence contradiction by A2, A7, A13, A15, TOPREAL9:8; :: thesis: verum

end;

Ball (p,r) c= Int cb by A2, TOPREAL9:16, TOPS_1:24;
then Int cb = Ball (p,r) by A5, XBOOLE_0:def 10;
then Fr (cl_Ball (p,r)) = (cl_Ball (p,r)) \ (Ball (p,r)) by TOPS_1:43;
hence Fr (cl_Ball (p,r)) = Sphere (p,r) by A4, A3, XBOOLE_1:88; :: thesis: verum