let n be Nat; :: thesis:
let a, r be Real; :: thesis:
let y, z, x be Point of (TOP-REAL n); :: thesis:
let S, T, Y be Element of REAL n; :: thesis:
assume A1: ( S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x ) ; :: thesis:
reconsider G = x as Point of (Euclid n) by TOPREAL3:8;
set s = y;
set t = z;
set X = ((1 / 2) * y) + ((1 / 2) * z);
assume that
A2: y <> z and
A3: y in Sphere (x,r) and
A4: z in cl_Ball (x,r) ; :: thesis:
A5: Ball (G,r) = Ball (x,r) by Th11;
A6: Sphere (x,r) c= cl_Ball (x,r) by Th15;

suppose A7: z in Sphere (x,r) ; :: thesis:

take z ; :: thesis:
thus ( z <> y & {y,z} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies z = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies z = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) by A2, A3, A7, Th34; :: thesis:

end;

suppose A8: not z in Sphere (x,r) ; :: thesis:

A9: now :: thesis:

assume A10: ((1 / 2) * y) + ((1 / 2) * z) = z ; :: thesis:
(z + (- ((1 / 2) * y))) + (- ((1 / 2) * z)) = (z - ((1 / 2) * y)) - ((1 / 2) * z)
.= z - z by A10, RLVECT_1:27
.= 0. (TOP-REAL n) by RLVECT_1:5 ;
then 0. (TOP-REAL n) = (z + (- ((1 / 2) * z))) + (- ((1 / 2) * y)) by RLVECT_1:def 3
.= ((1 * z) - ((1 / 2) * z)) - ((1 / 2) * y) by RLVECT_1:def 8
.= ((1 - (1 / 2)) * z) - ((1 / 2) * y) by RLVECT_1:35
.= (1 / 2) * (z - y) by RLVECT_1:34 ;
then z - y = 0. (TOP-REAL n) by RLVECT_1:11;
hence contradiction by A2, RLVECT_1:21; :: thesis:

end;

(Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by Th16;
then A11: z in Ball (G,r) by A4, A5, A8, XBOOLE_0:def 3;
set a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
A12: ( (1 / 2) + (1 / 2) = 1 & |.(1 / 2).| = 1 / 2 ) by ABSVALUE:def 1;
Ball (G,r) = Ball (x,r) by Th11;
then ((1 / 2) * y) + ((1 / 2) * z) in Ball (G,r) by A3, A6, A12, A11, Th22;
then consider e1 being Point of (TOP-REAL n) such that
A13: {e1} = (halfline ((((1 / 2) * y) + ((1 / 2) * z)),z)) /\ (Sphere (x,r)) and
A14: e1 = ((1 - (((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (((1 / 2) * y) + ((1 / 2) * z))) + ((((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) by A1, A5, A9, Th35;
take e1 ; :: thesis:
A15: e1 in {e1} by TARSKI:def 1;
then e1 in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) by A13, XBOOLE_0:def 4;
then consider l being Real such that
A16: e1 = ((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z) and
A17: 0 <= l ;

hereby :: thesis:

assume e1 = y ; :: thesis:
then 0. (TOP-REAL n) = (((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z)) - y by A16, RLVECT_1:5
.= ((((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z)) - y by RLVECT_1:def 5
.= (((1 - l) * ((1 / 2) * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z))) - y by RLVECT_1:def 3
.= (((1 - l) * ((1 / 2) * y)) - y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by RLVECT_1:def 3
.= (((1 - l) * ((1 / 2) * y)) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by RLVECT_1:def 8
.= ((((1 - l) * (1 / 2)) * y) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by RLVECT_1:def 7
.= ((((1 - l) * (1 / 2)) - 1) * y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by RLVECT_1:35
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by RLVECT_1:def 7
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) + l) * z) by RLVECT_1:def 6
.= ((- ((1 / 2) + (l * (1 / 2)))) * y) + (((1 / 2) + (l * (1 / 2))) * z)
.= (((1 / 2) + (l * (1 / 2))) * z) - (((1 / 2) + (l * (1 / 2))) * y) by RLVECT_1:79
.= ((1 / 2) + (l * (1 / 2))) * (z - y) by RLVECT_1:34 ;
then ( (1 / 2) + (l * (1 / 2)) = 0 or z - y = 0. (TOP-REAL n) ) by RLVECT_1:11;
hence contradiction by A2, A17, RLVECT_1:21; :: thesis:

end;

A18: y in halfline (y,z) by Th25;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

set o = (1 + l) / 2;
let m be object ; :: thesis:
assume m in {y,e1} ; :: thesis:
then A19: ( m = y or m = e1 ) by TARSKI:def 2;
e1 = (((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z) by A16, RLVECT_1:def 5
.= ((((1 - l) * (1 / 2)) * y) + ((1 - l) * ((1 / 2) * z))) + (l * z) by RLVECT_1:def 7
.= ((((1 - l) * (1 / 2)) * y) + (((1 - l) * (1 / 2)) * z)) + (l * z) by RLVECT_1:def 7
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by RLVECT_1:def 3
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) + l) * z) by RLVECT_1:def 6
.= ((1 - ((1 + l) / 2)) * y) + (((1 + l) / 2) * z) ;
then A20: e1 in halfline (y,z) by A17;
e1 in Sphere (x,r) by A13, A15, XBOOLE_0:def 4;
hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A3, A18, A19, A20, XBOOLE_0:def 4; :: thesis:

end;

hereby :: according to TARSKI:def 3 :: thesis:

let m be object ; :: thesis:
assume A21: m in (halfline (y,z)) /\ (Sphere (x,r)) ; :: thesis:
then A22: m in halfline (y,z) by XBOOLE_0:def 4;
A23: m in Sphere (x,r) by A21, XBOOLE_0:def 4;

per cases ;

suppose m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) ; :: thesis:

then m in (halfline ((((1 / 2) * y) + ((1 / 2) * z)),z)) /\ (Sphere (x,r)) by A23, XBOOLE_0:def 4;
then m = e1 by A13, TARSKI:def 1;
hence m in {y,e1} by TARSKI:def 2; :: thesis:

end;

suppose A24: not m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) ; :: thesis:

consider M being Real such that
A25: m = ((1 - M) * y) + (M * z) and
A26: 0 <= M by A22;

A27: now :: thesis:

set o = (2 * M) - 1;
assume M > 1 ; :: thesis:
then 2 * M > 2 * 1 by XREAL_1:68;
then A28: (2 * M) - 1 > (2 * 1) - 1 by XREAL_1:14;
((1 - ((2 * M) - 1)) * (((1 / 2) * y) + ((1 / 2) * z))) + (((2 * M) - 1) * z) = (((1 - ((2 * M) - 1)) * ((1 / 2) * y)) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by RLVECT_1:def 5
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by RLVECT_1:def 7
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + (((1 - ((2 * M) - 1)) * (1 / 2)) * z)) + (((2 * M) - 1) * z) by RLVECT_1:def 7
.= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) * z) + (((2 * M) - 1) * z)) by RLVECT_1:def 3
.= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) + ((2 * M) - 1)) * z) by RLVECT_1:def 6
.= m by A25 ;
hence contradiction by A24, A28; :: thesis:

end;

( |.(z - x).| <= r & |.(z - x).| <> r ) by A4, A8, Th6;
then |.(z - x).| < r by XXREAL_0:1;
then z in Ball (x,r) ;
then A29: (LSeg (y,z)) /\ (Sphere (x,r)) = {y} by A3, Th31;
m in LSeg (y,z) by A25, A26, A27;
then m in {y} by A23, A29, XBOOLE_0:def 4;
then m = y by TARSKI:def 1;
hence m in {y,e1} by TARSKI:def 2; :: thesis:

end;

thus ( ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) by A8, A14; :: thesis:

end;