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:29, RLTOPSP1:70;
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)

the carrier of (TOP-REAL n) = REAL n by EUCLID:22
.= n -tuples_on REAL ;
then reconsider xf = x, yf = y, zf = z as Element of n -tuples_on REAL ;
reconsider yyf = yf, zzf = zf, xxf = xf as Element of REAL n ;
reconsider y1 = y - x, z1 = z - x as FinSequence of REAL ;
set X = |((y - x),(z - x))|;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (y,z)) \ {y,z} or a in Ball (x,r) )
A5: Sum (sqr (zf - xf)) = Sum (sqr (zzf - xxf))
.= |.z1.| ^2 by Th5 ;
A6: |.(z - x).| ^2 = r ^2 by A2, Th9;
assume A7: a in (LSeg (y,z)) \ {y,z} ; :: thesis: a in Ball (x,r)
then reconsider R = a as Point of (TOP-REAL n) ;
A8: R in LSeg (y,z) by A7, XBOOLE_0:def 5;
then consider l being Real such that
A9: 0 <= l and
A10: l <= 1 and
A11: R = ((1 - l) * y) + (l * z) by JGRAPH_1:35;
set l1 = 1 - l;
reconsider W1 = (1 - l) * (y - x), W2 = l * (z - x) as Element of REAL n by EUCLID:22;
A12: Sum (sqr (yf - zf)) >= 0 by RVSUM_1:86;
reconsider Rf = R - x as FinSequence of REAL ;
A14: W1 + W2 = ((1 - l) * (y - x)) + (l * (z - x))
.= (((1 - l) * y) - ((1 - l) * x)) + (l * (z - x)) by EUCLID:49
.= (((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x)) by EUCLID:49
.= ((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x) by EUCLID:45
.= ((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x) by JORDAN2C:7
.= (((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x)) by EUCLID:46
.= (((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x)) by EUCLID:50
.= (((1 - l) * y) + (l * z)) - (1 * x) by EUCLID:48
.= Rf by A11, EUCLID:29 ;
reconsider W1 = W1, W2 = W2 as Element of n -tuples_on REAL ;
A15: mlt (W1,W2) = mlt (((1 - l) * (y - x)),(l * (z - x)))
.= mlt (((1 - l) * (y - x)),(l * (zzf - xxf)))
.= mlt (((1 - l) * (yyf - xxf)),(l * (zzf - xxf)))
.= (1 - l) * (mlt ((yf - xf),(l * (zf - xf)))) by RVSUM_1:65 ;
A17: sqr W1 = sqr ((1 - l) * (y - x))
.= sqr ((1 - l) * (yf - xf))
.= ((1 - l) ^2) * (sqr (yf - xf)) by RVSUM_1:58 ;
Sum (sqr Rf) >= 0 by RVSUM_1:86;
then |.(R - x).| ^2 = Sum (sqr Rf) by SQUARE_1:def 2
.= Sum (((sqr W1) + (2 * (mlt (W1,W2)))) + (sqr W2)) by A14, RVSUM_1:68
.= (Sum ((sqr W1) + (2 * (mlt (W1,W2))))) + (Sum (sqr W2)) by RVSUM_1:89
.= ((Sum (sqr W1)) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr W2)) by RVSUM_1:89
.= ((Sum (((1 - l) ^2) * (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr (l * (zf - xf)))) by A17
.= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr (l * (zf - xf)))) by RVSUM_1:87
.= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum ((l ^2) * (sqr (zf - xf)))) by RVSUM_1:58
.= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (Sum (sqr (zf - xf)))) by RVSUM_1:87
.= ((((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 A1, A5, Th9
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum (mlt (W1,W2))))) + ((l ^2) * (r ^2)) by A6, RVSUM_1:87
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum ((1 - l) * (mlt ((yf - xf),(l * (zf - xf)))))))) + ((l ^2) * (r ^2)) by A15
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum ((1 - l) * (l * (mlt ((yf - xf),(zf - xf)))))))) + ((l ^2) * (r ^2)) by RVSUM_1:65
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum (((1 - l) * l) * (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2)) by RVSUM_1:49
.= ((((1 - l) ^2) * (r ^2)) + (2 * (((1 - l) * l) * (Sum (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2)) by RVSUM_1:87
.= ((((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 RVSUM_1:def 16
.= ((((1 - (2 * l)) + (l ^2)) + (l ^2)) * (r ^2)) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|) ;
then A18: (|.(R - x).| ^2) - (r ^2) = ((2 * l) * (1 - l)) * ((- (r ^2)) + |((y - x),(z - x))|) ;

now

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

end;

then A20: 2 * l > 0 by A9, XREAL_1:129;

A21: now

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

end;

1 - 1 <= 1 - l by A10, XREAL_1:13;
then A22: (2 * l) * (1 - l) > 0 by A20, A21, XREAL_1:129;
A23: |.(y - x).| ^2 = r ^2 by A1, Th9;

A24: now

assume |.(R - x).| = r ; :: thesis: contradiction
then |((y - x),(z - x))| - (r ^2) = 0 by A18, A22, XCMPLX_1:6;
then 0 = ((|.(y - x).| ^2) - (2 * |((y - x),(z - x))|)) + (|.(z - x).| ^2) by A2, A23, Th9
.= |.((y - x) - (z - x)).| ^2 by EUCLID_2:46
.= |.(((y - x) - z) + x).| ^2 by EUCLID:47
.= |.(((y - x) + x) - z).| ^2 by JORDAN2C:7
.= |.(yf - zf).| ^2 by EUCLID:48
.= Sum (sqr (yf - zf)) by A12, SQUARE_1:def 2 ;
then yf - zf = n |-> 0 by RVSUM_1:91;
hence contradiction by A3, RVSUM_1:38; :: thesis: verum

end;

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 |.(R - x).| <= r by A8, Th8;
then |.(R - x).| < r by A24, XXREAL_0:1;
hence a in Ball (x,r) ; :: thesis: verum

end;

end;