let n be Element of NAT ; :: thesis: for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) \ {y,z} c= Ball x,r
let r be real number ; :: thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) \ {y,z} c= Ball x,r
let y, x, z be Point of (TOP-REAL n); :: thesis: ( y in Sphere x,r & z in Sphere x,r implies (LSeg y,z) \ {y,z} c= Ball x,r )
assume that
A1: y in Sphere x,r and
A2: z in Sphere x,r ; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r

per cases ( y = z or y <> z ) ;

suppose y = z ; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r

then ( LSeg y,z = {y} & {y,z} = {y} ) by ENUMSET1:69, TOPREAL1:7;
then (LSeg y,z) \ {y,z} = {} by XBOOLE_1:37;
hence (LSeg y,z) \ {y,z} c= Ball x,r by XBOOLE_1:2; :: thesis: verum

end;

suppose A3: y <> z ; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg y,z) \ {y,z} or a in Ball x,r )
assume A4: a in (LSeg y,z) \ {y,z} ; :: thesis: a in Ball x,r
then reconsider R = a as Point of (TOP-REAL n) ;
A5: R in LSeg y,z by A4, XBOOLE_0:def 5;
then consider l being Real such that
A6: 0 <= l and
A7: l <= 1 and
A8: R = ((1 - l) * y) + (l * z) by JGRAPH_1:52;
set l1 = 1 - l;
set X = |((y - x),(z - x))|;
reconsider xf = x, yf = y, zf = z as Element of n -tuples_on REAL by EUCLID:25;
reconsider y1 = y - x, z1 = z - x as FinSequence of REAL by EUCLID:27;
reconsider Rf = R - x as FinSequence of REAL by EUCLID:27;
A9: Sum (sqr Rf) >= 0 by RVSUM_1:116;
A10: |.(y - x).| ^2 = r ^2 by A1, Th9;
A11: |.(z - x).| ^2 = r ^2 by A2, Th9;
reconsider W1 = (1 - l) * (y - x), W2 = l * (z - x) as Element of n -tuples_on REAL by EUCLID:25;
A12: W1 + W2 = (((1 - l) * y) - ((1 - l) * x)) + (l * (z - x)) by EUCLID:53
.= (((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x)) by EUCLID:53
.= ((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x) by EUCLID:49
.= ((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x) by JORDAN2C:9
.= (((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x)) by EUCLID:50
.= (((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x)) by EUCLID:54
.= (((1 - l) * y) + (l * z)) - (1 * x) by EUCLID:52
.= Rf by A8, EUCLID:33 ;
|.(R - x).| ^2 = Sum (sqr Rf) by A9, SQUARE_1:def 4
.= Sum (((sqr W1) + (2 * (mlt W1,W2))) + (sqr W2)) by A12, RVSUM_1:98
.= (Sum ((sqr W1) + (2 * (mlt W1,W2)))) + (Sum (sqr W2)) by RVSUM_1:119
.= ((Sum (sqr W1)) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr W2)) by RVSUM_1:119
.= ((Sum (((1 - l) ^2 ) * (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr (l * (zf - xf)))) by RVSUM_1:84
.= ((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr (l * (zf - xf)))) by RVSUM_1:117
.= ((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum ((l ^2 ) * (sqr (zf - xf)))) by RVSUM_1:84
.= ((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (Sum (sqr (zf - xf)))) by RVSUM_1:117
.= ((((1 - l) ^2 ) * (|.y1.| ^2 )) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (Sum (sqr (zf - xf)))) by Th5
.= ((((1 - l) ^2 ) * (r ^2 )) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (|.z1.| ^2 )) by A10, Th5
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum (mlt W1,W2)))) + ((l ^2 ) * (r ^2 )) by A11, RVSUM_1:117
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum ((1 - l) * (mlt (yf - xf),(l * (zf - xf))))))) + ((l ^2 ) * (r ^2 )) by RVSUM_1:94
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum ((1 - l) * (l * (mlt (yf - xf),(zf - xf))))))) + ((l ^2 ) * (r ^2 )) by RVSUM_1:94
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum (((1 - l) * l) * (mlt (yf - xf),(zf - xf)))))) + ((l ^2 ) * (r ^2 )) by RVSUM_1:71
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (((1 - l) * l) * (Sum (mlt (yf - xf),(zf - xf)))))) + ((l ^2 ) * (r ^2 )) by RVSUM_1:117
.= ((((1 - l) ^2 ) * (r ^2 )) + (((2 * (1 - l)) * l) * (Sum (mlt (yf - xf),(zf - xf))))) + ((l ^2 ) * (r ^2 ))
.= ((((1 - l) ^2 ) * (r ^2 )) + (((2 * (1 - l)) * l) * |((y - x),(z - x))|)) + ((l ^2 ) * (r ^2 )) by EUCLID_2:def 1
.= ((((1 - (2 * l)) + (l ^2 )) + (l ^2 )) * (r ^2 )) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|) ;
then A13: (|.(R - x).| ^2 ) - (r ^2 ) = ((2 * l) * (1 - l)) * ((- (r ^2 )) + |((y - x),(z - x))|) ;
Sphere x,r c= cl_Ball x,r by Th17;
then LSeg y,z c= cl_Ball x,r by A1, A2, JORDAN1:def 1;
then A14: |.(R - x).| <= r by A5, Th8;

now

assume l = 0 ; :: thesis: contradiction
then R = y by A8, Th4;
then R in {y,z} by TARSKI:def 2;
hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

end;

then A15: 2 * l > 0 by A6, XREAL_1:131;
A16: 1 - 1 <= 1 - l by A7, XREAL_1:15;

now

assume 1 - l = 0 ; :: thesis: contradiction
then R = z by A8, Th4;
then R in {y,z} by TARSKI:def 2;
hence contradiction by A4, XBOOLE_0:def 5; :: thesis: verum

end;

then A17: (2 * l) * (1 - l) > 0 by A15, A16, XREAL_1:131;
A18: Sum (sqr (yf - zf)) >= 0 by RVSUM_1:116;

now

assume |.(R - x).| = r ; :: thesis: contradiction
then |((y - x),(z - x))| - (r ^2 ) = 0 by A13, A17, XCMPLX_1:6;
then 0 = ((|.(y - x).| ^2 ) - (2 * |((y - x),(z - x))|)) + (|.(z - x).| ^2 ) by A10, A11
.= |.((y - x) - (z - x)).| ^2 by EUCLID_2:68
.= |.(((y - x) - z) + x).| ^2 by EUCLID:51
.= |.(((y - x) + x) - z).| ^2 by JORDAN2C:9
.= |.(yf - zf).| ^2 by EUCLID:52
.= Sum (sqr (yf - zf)) by A18, SQUARE_1:def 4 ;
then yf - zf = n |-> 0 by RVSUM_1:121;
hence contradiction by A3, RVSUM_1:59; :: thesis: verum

end;

then |.(R - x).| < r by A14, XXREAL_0:1;
hence a in Ball x,r ; :: thesis: verum

end;

end;