let n be Nat; :: thesis: for r being Real
for y, z, x 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; :: thesis: for y, z, x 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, z, x 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) ; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (y,z)) \ {y,z} or a in Ball (x,r) )
A4: Sum (sqr (zf - xf)) = |.z1.| ^2 by Th3;
A5: |.(z - x).| ^2 = r ^2 by A2, Th7;
assume A6: a in (LSeg (y,z)) \ {y,z} ; :: thesis: a in Ball (x,r)
then reconsider R = a as Point of (TOP-REAL n) ;
A7: R in LSeg (y,z) by A6, XBOOLE_0:def 5;
then consider l being Real such that
A8: 0 <= l and
A9: l <= 1 and
A10: R = ((1 - l) * y) + (l * z) by RLTOPSP1:76;
set l1 = 1 - l;
reconsider W1 = (1 - l) * (y - x), W2 = l * (z - x) as Element of REAL n by EUCLID:22;
A11: Sum (sqr (yf - zf)) >= 0 by RVSUM_1:86;
reconsider Rf = R - x as FinSequence of REAL ;
A12: W1 + W2 = (((1 - l) * y) - ((1 - l) * x)) + (l * (z - x)) by RLVECT_1:34
.= (((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x)) by RLVECT_1:34
.= ((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x) by RLVECT_1:def 3
.= ((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x) by RLVECT_1:def 3
.= (((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x)) by RLVECT_1:27
.= (((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x)) by RLVECT_1:35
.= (((1 - l) * y) + (l * z)) - (1 * x) by RLVECT_4:1
.= Rf by A10, RLVECT_1:def 8 ;
reconsider W1 = W1, W2 = W2 as Element of n -tuples_on REAL ;
A13: mlt (W1,W2) = (1 - l) * (mlt ((yf - xf),(l * (zf - xf)))) by RVSUM_1:65;
A14: sqr W1 = ((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 A12, 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
.= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr (l * (zf - xf)))) by A14, 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 Th3
.= ((((1 - l) ^2) * (r ^2)) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (|.z1.| ^2)) by A1, A4, Th7
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum (mlt (W1,W2))))) + ((l ^2) * (r ^2)) by A5, RVSUM_1:87
.= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum ((1 - l) * (l * (mlt ((yf - xf),(zf - xf)))))))) + ((l ^2) * (r ^2)) by A13, 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 A15: (|.(R - x).| ^2) - (r ^2) = ((2 * l) * (1 - l)) * ((- (r ^2)) + |((y - x),(z - x))|) ;

now :: thesis: not l = 0

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

end;

then A16: 2 * l > 0 by A8, XREAL_1:129;

A17: now :: thesis: not 1 - l = 0

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

end;

1 - 1 <= 1 - l by A9, XREAL_1:13;
then A18: (2 * l) * (1 - l) > 0 by A16, A17, XREAL_1:129;
A19: |.(y - x).| ^2 = r ^2 by A1, Th7;

A20: now :: thesis: not |.(R - x).| = r

assume |.(R - x).| = r ; :: thesis: contradiction
then |((y - x),(z - x))| - (r ^2) = 0 by A15, A18, XCMPLX_1:6;
then 0 = ((|.(y - x).| ^2) - (2 * |((y - x),(z - x))|)) + (|.(z - x).| ^2) by A2, A19, Th7
.= |.((y - x) - (z - x)).| ^2 by EUCLID_2:46
.= |.(((y - x) - z) + x).| ^2 by RLVECT_1:29
.= |.(((y - x) + x) - z).| ^2 by RLVECT_1:def 3
.= |.(yf - zf).| ^2 by RLVECT_4:1
.= Sum (sqr (yf - zf)) by A11, 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 Th15;
then LSeg (y,z) c= cl_Ball (x,r) by A1, A2, JORDAN1:def 1;
then |.(R - x).| <= r by A7, Th6;
then |.(R - x).| < r by A20, XXREAL_0:1;
hence a in Ball (x,r) ; :: thesis: verum

end;

end;