let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n)
for r being non zero real number holds Cl (Ball x,r) = cl_Ball x,r
let x be Point of (TOP-REAL n); :: thesis: for r being non zero real number holds Cl (Ball x,r) = cl_Ball x,r
let r be non zero real number ; :: thesis: Cl (Ball x,r) = cl_Ball x,r
thus Cl (Ball x,r) c= cl_Ball x,r by TOPREAL9:16, TOPS_1:31; :: according to XBOOLE_0:def 10 :: thesis: cl_Ball x,r c= Cl (Ball x,r)

per cases ( Ball x,r is empty or not Ball x,r is empty ) ;

suppose A1: Ball x,r is empty ; :: thesis: cl_Ball x,r c= Cl (Ball x,r)

then r < 0 ;
then A2: cl_Ball x,r is empty ;
thus cl_Ball x,r c= Cl (Ball x,r) by A1, A2; :: thesis: verum

end;

suppose A3: not Ball x,r is empty ; :: thesis: cl_Ball x,r c= Cl (Ball x,r)

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in cl_Ball x,r or a in Cl (Ball x,r) )
assume A4: a in cl_Ball x,r ; :: thesis: a in Cl (Ball x,r)
then reconsider a = a as Point of (TOP-REAL n) ;
reconsider ae = a as Point of (Euclid n) by TOPREAL3:13;
A5: 0 < r by A3;
for s being real number st 0 < s & s < r holds
Ball ae,s meets Ball x,r

proof

let s be real number ; :: thesis: ( 0 < s & s < r implies Ball ae,s meets Ball x,r )
assume that
A6: 0 < s and
A7: s < r ; :: thesis: Ball ae,s meets Ball x,r

now

A8: (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r by TOPREAL9:18;

per cases ( a in Ball x,r or a in Sphere x,r ) by A4, A8, XBOOLE_0:def 3;

suppose A9: a in Ball x,r ; :: thesis: Ball a,s meets Ball x,r

|.(a - a).| = 0 by TOPRNS_1:29;
then a in Ball a,s by A6, TOPREAL9:7;
hence Ball a,s meets Ball x,r by A9, XBOOLE_0:3; :: thesis: verum

end;

suppose A10: a in Sphere x,r ; :: thesis: Ball a,s meets Ball x,r

then A11: |.(a - x).| = r by TOPREAL9:9;
|.(x - x).| = 0 by TOPRNS_1:29;
then A12: x in Ball x,r by A5, TOPREAL9:7;
set z = s / (2 * r);
set q = ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x);
1 * r < 2 * r by A5, XREAL_1:70;
then s < 2 * r by A7, XXREAL_0:2;
then A13: s / (2 * r) < 1 by A6, XREAL_1:191;
0 < 2 * r by A5, XREAL_1:131;
then A14: 0 < s / (2 * r) by A6, XREAL_1:141;
then A15: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in LSeg a,x by A13;
Ball x,r misses Sphere x,r by TOPREAL9:19;
then a <> x by A10, A12, XBOOLE_0:3;
then ( ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> a & ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> x ) by A13, A14, TOPREAL9:4;
then not ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in {a,x} by TARSKI:def 2;
then A16: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in (LSeg a,x) \ {a,x} by A15, XBOOLE_0:def 5;
A17: (LSeg a,x) \ {a,x} c= Ball x,r by A10, Th20;
(((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x)) - a = (((1 - (s / (2 * r))) * a) - a) + ((s / (2 * r)) * x) by JORDAN2C:9
.= (((1 * a) - ((s / (2 * r)) * a)) - a) + ((s / (2 * r)) * x) by EUCLID:54
.= ((a - ((s / (2 * r)) * a)) - a) + ((s / (2 * r)) * x) by EUCLID:33
.= ((a - a) - ((s / (2 * r)) * a)) + ((s / (2 * r)) * x) by TOPREAL9:1
.= ((0. (TOP-REAL n)) - ((s / (2 * r)) * a)) + ((s / (2 * r)) * x) by EUCLID:46
.= ((s / (2 * r)) * x) - ((s / (2 * r)) * a) by EUCLID:31
.= (s / (2 * r)) * (x - a) by EUCLID:53 ;
then |.((((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x)) - a).| = (abs (s / (2 * r))) * |.(x - a).| by TOPRNS_1:8
.= (s / (2 * r)) * |.(x - a).| by A14, ABSVALUE:def 1
.= (s / (2 * r)) * |.(a - x).| by TOPRNS_1:28
.= s / 2 by A11, XCMPLX_1:93 ;
then A18: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in Sphere a,(s / 2) by TOPREAL9:9;
s / 2 < s / 1 by A6, XREAL_1:78;
then Sphere a,(s / 2) c= Ball a,s by Th22;
hence Ball a,s meets Ball x,r by A16, A17, A18, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence Ball ae,s meets Ball x,r by TOPREAL9:13; :: thesis: verum

end;

hence a in Cl (Ball x,r) by A5, GOBOARD6:96; :: thesis: verum

end;

end;