let n be Element of NAT ; :: thesis:
let r, a be real number ; :: 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 Th13;
A6: Sphere (x,r) c= cl_Ball (x,r) by Th17;

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, Th36; :: thesis:

end;

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

A9: now

assume ((1 / 2) * y) + ((1 / 2) * z) = z ; :: thesis:
then (z - ((1 / 2) * y)) - ((1 / 2) * z) = z - z by EUCLID:46
.= 0. (TOP-REAL n) by EUCLID:42 ;
then 0. (TOP-REAL n) = (z - ((1 / 2) * z)) - ((1 / 2) * y) by JORDAN2C:7
.= ((1 * z) - ((1 / 2) * z)) - ((1 / 2) * y) by EUCLID:29
.= ((1 - (1 / 2)) * z) - ((1 / 2) * y) by EUCLID:50
.= (1 / 2) * (z - y) by EUCLID:49 ;
then z - y = 0. (TOP-REAL n) by EUCLID:31;
hence contradiction by A2, EUCLID:43; :: thesis:

end;

(Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by Th18;
then A10: 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))));
A11: ( (1 / 2) + (1 / 2) = 1 & abs (1 / 2) = 1 / 2 ) by ABSVALUE:def 1;
Ball (G,r) = Ball (x,r) by Th13;
then ((1 / 2) * y) + ((1 / 2) * z) in Ball (G,r) by A3, A6, A11, A10, Th24;
then consider e1 being Point of (TOP-REAL n) such that
A12: {e1} = (halfline ((((1 / 2) * y) + ((1 / 2) * z)),z)) /\ (Sphere (x,r)) and
A13: 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, Th37;
take e1 ; :: thesis:
A14: e1 in {e1} by TARSKI:def 1;
then e1 in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) by A12, XBOOLE_0:def 4;
then consider l being real number such that
A15: e1 = ((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z) and
A16: 0 <= l by Th26;

hereby :: thesis:

assume e1 = y ; :: thesis:
then 0. (TOP-REAL n) = (((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z)) - y by A15, EUCLID:42
.= ((((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z)) - y by EUCLID:32
.= (((1 - l) * ((1 / 2) * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z))) - y by EUCLID:26
.= (((1 - l) * ((1 / 2) * y)) - y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by JORDAN2C:7
.= (((1 - l) * ((1 / 2) * y)) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:29
.= ((((1 - l) * (1 / 2)) * y) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:30
.= ((((1 - l) * (1 / 2)) - 1) * y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:50
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:30
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:33
.= (((- 1) * ((1 / 2) + (l * (1 / 2)))) * y) + (((1 / 2) + (l * (1 / 2))) * z)
.= ((- ((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 EUCLID:40
.= (((1 / 2) + (l * (1 / 2))) * z) - (((1 / 2) + (l * (1 / 2))) * y)
.= ((1 / 2) + (l * (1 / 2))) * (z - y) by EUCLID:49 ;
then ( (1 / 2) + (l * (1 / 2)) = 0 or z - y = 0. (TOP-REAL n) ) by EUCLID:31;
hence contradiction by A2, A16, EUCLID:43; :: thesis:

end;

A17: y in halfline (y,z) by Th27;

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

set o = (1 + l) / 2;
let m be set ; :: thesis:
assume m in {y,e1} ; :: thesis:
then A18: ( m = y or m = e1 ) by TARSKI:def 2;
e1 = (((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z) by A15, EUCLID:32
.= ((((1 - l) * (1 / 2)) * y) + ((1 - l) * ((1 / 2) * z))) + (l * z) by EUCLID:30
.= ((((1 - l) * (1 / 2)) * y) + (((1 - l) * (1 / 2)) * z)) + (l * z) by EUCLID:30
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:26
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:33
.= ((1 - ((1 + l) / 2)) * y) + (((1 + l) / 2) * z) ;
then A19: e1 in halfline (y,z) by A16;
e1 in Sphere (x,r) by A12, A14, XBOOLE_0:def 4;
hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A3, A17, A18, A19, XBOOLE_0:def 4; :: thesis:

end;

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

let m be set ; :: thesis:
assume A20: m in (halfline (y,z)) /\ (Sphere (x,r)) ; :: thesis:
then A21: m in halfline (y,z) by XBOOLE_0:def 4;
A22: m in Sphere (x,r) by A20, 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 A22, XBOOLE_0:def 4;
then m = e1 by A12, TARSKI:def 1;
hence m in {y,e1} by TARSKI:def 2; :: thesis:

end;

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

consider M being real number such that
A24: m = ((1 - M) * y) + (M * z) and
A25: 0 <= M by A21, Th26;

A26: now

set o = (2 * M) - 1;
assume M > 1 ; :: thesis:
then 2 * M > 2 * 1 by XREAL_1:68;
then A27: (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 EUCLID:32
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by EUCLID:30
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + (((1 - ((2 * M) - 1)) * (1 / 2)) * z)) + (((2 * M) - 1) * z) by EUCLID:30
.= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) * z) + (((2 * M) - 1) * z)) by EUCLID:26
.= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) + ((2 * M) - 1)) * z) by EUCLID:33
.= m by A24 ;
hence contradiction by A23, A27; :: thesis:

end;

( |.(z - x).| <= r & |.(z - x).| <> r ) by A4, A8, Th8;
then |.(z - x).| < r by XXREAL_0:1;
then z in Ball (x,r) ;
then A28: (LSeg (y,z)) /\ (Sphere (x,r)) = {y} by A3, Th33;
M is Real by XREAL_0:def 1;
then m in LSeg (y,z) by A24, A25, A26;
then m in {y} by A22, A28, 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, A13; :: thesis:

end;