let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real 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 st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let r be Real; :: 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: Ball (p,r) misses Sphere (p,r) by TOPREAL9:19;
A3: (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) by TOPREAL9:18;
A4: Int cb c= Ball (p,r)

proof

reconsider ONE = 1 as Real ;
let x be object ; :: 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
A5: Q is open and
A6: Q c= cl_Ball (p,r) and
A7: x in Q by TOPS_1:22;
reconsider q = x as Point of (TOP-REAL n) by A7;
consider w being positive Real such that
A8: Ball (q,w) c= Q by A5, A7, TOPS_4:2;
assume not x in Ball (p,r) ; :: thesis: contradiction
then q in Sphere (p,r) by A3, A6, A7, XBOOLE_0:def 3;
then A9: |.(q - p).| = r by TOPREAL9:9;
set w2 = w / 2;
set wr = ((w / 2) / r) * (q - p);
A10: |.((w / 2) / r).| = (w / 2) / r by A1, ABSVALUE:def 1;
A11: ((((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 RLVECT_1:def 3
.= |.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).| by RLVECT_1:15
.= |.(((w / 2) / r) * (q - p)).|
.= ((w / 2) / r) * r by A9, A10, 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 A12: (((w / 2) / r) * (q - p)) + q in Q by A8;
A13: ((w / 2) / r) + ONE = ((w / 2) / r) + (r / r) by A1, XCMPLX_1:60
.= ((w / 2) + r) / r ;
A14: (w / 2) + r > 0 + r by XREAL_1:6;
|.(((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 A9, A13, A11, TOPRNS_1:7
.= (w / 2) + r by A1, XCMPLX_1:87 ;
hence contradiction by A6, A12, A14, TOPREAL9:8; :: thesis: verum

end;

Ball (p,r) c= Int cb by TOPREAL9:16, TOPS_1:24;
then Int cb = Ball (p,r) by A4, 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 A3, A2, XBOOLE_1:88; :: thesis: verum