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:
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:
reconsider G = x as Point of (Euclid n) by TOPREAL3:13;
A5: Ball G,r = Ball x,r by Th13;
A6: Sphere x,r c= cl_Ball x,r by Th17;

per cases ;

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

take e1 = z; :: thesis:
thus ( e1 <> y & {y,e1} = (halfline y,z) /\ (Sphere x,r) & ( 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 A2, A3, A7, Th36; :: thesis:

end;

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

A9: (1 / 2) + (1 / 2) = 1 ;
A10: abs (1 / 2) = 1 / 2 by ABSVALUE:def 1;
A11: Ball G,r = Ball x,r by Th13;
(Ball x,r) \/ (Sphere x,r) = cl_Ball x,r by Th18;
then z in Ball G,r by A4, A5, A8, XBOOLE_0:def 3;
then A12: ((1 / 2) * y) + ((1 / 2) * z) in Ball G,r by A3, A6, A9, A10, A11, Th24;

A13: now

assume ((1 / 2) * y) + ((1 / 2) * z) = z ; :: thesis:
then (z - ((1 / 2) * y)) - ((1 / 2) * z) = z - z by EUCLID:50
.= 0. (TOP-REAL n) by EUCLID:46 ;
then 0. (TOP-REAL n) = (z - ((1 / 2) * z)) - ((1 / 2) * y) by Th1
.= ((1 * z) - ((1 / 2) * z)) - ((1 / 2) * y) by EUCLID:33
.= ((1 - (1 / 2)) * z) - ((1 / 2) * y) by EUCLID:54
.= (1 / 2) * (z - y) by EUCLID:53 ;
then z - y = 0. (TOP-REAL n) by EUCLID:35;
hence contradiction by A2, EUCLID:47; :: thesis:

end;

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))));
consider e1 being Point of (TOP-REAL n) such that
A14: {e1} = (halfline (((1 / 2) * y) + ((1 / 2) * z)),z) /\ (Sphere x,r) and
A15: 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, A12, A13, Th37;
take e1 ; :: thesis:
A16: e1 in {e1} by TARSKI:def 1;
then e1 in halfline (((1 / 2) * y) + ((1 / 2) * z)),z by A14, XBOOLE_0:def 4;
then consider l being real number such that
A17: e1 = ((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z) and
A18: 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 A17, EUCLID:46
.= ((((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z)) - y by EUCLID:36
.= (((1 - l) * ((1 / 2) * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z))) - y by EUCLID:30
.= (((1 - l) * ((1 / 2) * y)) - y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by JORDAN2C:9
.= (((1 - l) * ((1 / 2) * y)) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:33
.= ((((1 - l) * (1 / 2)) * y) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:34
.= ((((1 - l) * (1 / 2)) - 1) * y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:54
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:34
.= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:37
.= (((- 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) by EUCLID:43
.= (((1 / 2) + (l * (1 / 2))) * z) + (- (((1 / 2) + (l * (1 / 2))) * y)) by EUCLID:44
.= (((1 / 2) + (l * (1 / 2))) * z) - (((1 / 2) + (l * (1 / 2))) * y) by EUCLID:34
.= ((1 / 2) + (l * (1 / 2))) * (z - y) by EUCLID:53 ;
then ( (1 / 2) + (l * (1 / 2)) = 0 or z - y = 0. (TOP-REAL n) ) by EUCLID:35;
then (1 + l) - 1 = 0 - 1 by A2, EUCLID:47;
hence contradiction by A18; :: thesis:

end;

A19: y in halfline y,z by Th27;

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

let m be set ; :: thesis:
assume m in {y,e1} ; :: thesis:
then A20: ( m = y or m = e1 ) by TARSKI:def 2;
set o = (1 + l) / 2;
A21: e1 = (((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z) by A17, EUCLID:36
.= ((((1 - l) * (1 / 2)) * y) + ((1 - l) * ((1 / 2) * z))) + (l * z) by EUCLID:34
.= ((((1 - l) * (1 / 2)) * y) + (((1 - l) * (1 / 2)) * z)) + (l * z) by EUCLID:34
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:30
.= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:37
.= ((1 - ((1 + l) / 2)) * y) + (((1 + l) / 2) * z) ;
1 + 0 <= 1 + l by A18, XREAL_1:8;
then 0 <= (1 + l) / 2 ;
then A22: e1 in halfline y,z by A21;
e1 in Sphere x,r by A14, A16, XBOOLE_0:def 4;
hence m in (halfline y,z) /\ (Sphere x,r) by A3, A19, A20, A22, XBOOLE_0:def 4; :: thesis:

end;

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

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

end;

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

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

A28: now

set o = (2 * M) - 1;
assume M > 1 ; :: thesis:
then 2 * M > 2 * 1 by XREAL_1:70;
then A29: (2 * M) - 1 > (2 * 1) - 1 by XREAL_1:16;
((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:36
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by EUCLID:34
.= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + (((1 - ((2 * M) - 1)) * (1 / 2)) * z)) + (((2 * M) - 1) * z) by EUCLID:34
.= (((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)) + ((2 * M) - 1)) * z) by EUCLID:37
.= m by A26 ;
hence contradiction by A25, A29; :: thesis:

end;

A30: |.(z - x).| <= r by A4, Th8;
|.(z - x).| <> r by A8;
then |.(z - x).| < r by A30, XXREAL_0:1;
then z in Ball x,r ;
then A31: (LSeg y,z) /\ (Sphere x,r) = {y} by A3, Th33;
A32: M is Real by XREAL_0:def 1;
LSeg y,z = { (((1 - d) * y) + (d * z)) where d is Real : ( 0 <= d & d <= 1 ) } ;
then m in LSeg y,z by A26, A27, A28, A32;
then m in {y} by A24, A31, 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, A15; :: thesis:

end;