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:13;
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 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: 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 JORDAN2C:9
.= ((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;

(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: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)
.= (((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)
.= ((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;
hence contradiction by A2, A16, EUCLID:47; :: 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: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) ;
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:70;
then A27: (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 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;