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 Ball x,r is empty ; :: thesis: cl_Ball x,r c= Cl (Ball x,r)

then r < 0 ;
hence cl_Ball x,r c= Cl (Ball x,r) ; :: thesis: verum

end;

suppose A1: 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 A2: 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;
A3: 0 < r by A1;
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
A4: 0 < s and
A5: s < r ; :: thesis: Ball ae,s meets Ball x,r

now

A6: (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 A2, A6, XBOOLE_0:def 3;

suppose A7: 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 A4, TOPREAL9:7;
hence Ball a,s meets Ball x,r by A7, XBOOLE_0:3; :: thesis: verum

end;

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

then A9: |.(a - x).| = r by TOPREAL9:9;
|.(x - x).| = 0 by TOPRNS_1:29;
then A10: x in Ball x,r by A3, TOPREAL9:7;
set z = s / (2 * r);
set q = ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x);
1 * r < 2 * r by A3, XREAL_1:70;
then s < 2 * r by A5, XXREAL_0:2;
then A11: s / (2 * r) < 1 by A4, XREAL_1:191;
0 < 2 * r by A3, XREAL_1:131;
then A12: 0 < s / (2 * r) by A4, XREAL_1:141;
A13: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in LSeg a,x by A3, A4, A11;
Ball x,r misses Sphere x,r by TOPREAL9:19;
then A14: a <> x by A8, A10, XBOOLE_0:3;
then A15: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> a by A12, TOPREAL9:4;
((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> x by A11, A14, TOPREAL9:4;
then not ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in {a,x} by A15, TARSKI:def 2;
then A16: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in (LSeg a,x) \ {a,x} by A13, XBOOLE_0:def 5;
A17: (LSeg a,x) \ {a,x} c= Ball x,r by A8, 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 A3, A4, ABSVALUE:def 1
.= (s / (2 * r)) * |.(a - x).| by TOPRNS_1:28
.= s / 2 by A9, 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 A4, 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 A3, GOBOARD6:96; :: thesis: verum

end;

end;