let n be Element of NAT ; :: thesis: for r, a being real number
for y, z, x being Point of (TOP-REAL n)
for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let r, a be real number ; :: thesis: for y, z, x being Point of (TOP-REAL n)
for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let y, z, x be Point of (TOP-REAL n); :: thesis: for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let S, T, X be Element of REAL n; :: thesis: ( S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) )
assume that
A1: S = y and
A2: T = z and
A3: X = x ; :: thesis: ( not y <> z or not y in Ball (x,r) or not a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) )
set s = y;
set t = z;
A4: |.(y - x).| = sqrt (Sum (sqr (S - X))) by A1, A3;
A5: y - x = S - X by A1, A3;
A6: Sum (sqr (T - S)) >= 0 by RVSUM_1:86;
then A7: |.(T - S).| ^2 = Sum (sqr (T - S)) by SQUARE_1:def 2;
set A = Sum (sqr (T - S));
assume that
A8: y <> z and
A9: y in Ball (x,r) and
A10: a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
A11: |.(T - S).| <> 0 by A1, A2, A8, EUCLID:16;

A12: now

assume Sum (sqr (T - S)) <= 0 ; :: thesis: contradiction
then Sum (sqr (T - S)) = 0 by RVSUM_1:86;
hence contradiction by A11, SQUARE_1:17; :: thesis: verum

end;

set C = (Sum (sqr (S - X))) - (r ^2);
set B = 2 * |((z - y),(y - x))|;
A13: ( r = 0 or r <> 0 ) ;
Sum (sqr (S - X)) >= 0 by RVSUM_1:86;
then A14: |.(S - X).| ^2 = Sum (sqr (S - X)) by SQUARE_1:def 2;
|.(y - x).| < r by A9, Th7;
then (sqrt (Sum (sqr (S - X)))) ^2 < r ^2 by A4, SQUARE_1:16;
then A15: (Sum (sqr (S - X))) - (r ^2) < 0 by A14, XREAL_1:49;
then A16: ((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) < 0 by A12, XREAL_1:141;
set l2 = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
set l1 = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
take e1 = ((1 - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * y) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z); :: thesis: ( {e1} = (halfline (y,z)) /\ (Sphere (x,r)) & e1 = ((1 - a) * y) + (a * z) )
A17: 0 <= - (- r) by A9;
A18: ( delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2))) = ((2 * |((z - y),(y - x))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2))) & (2 * |((z - y),(y - x))|) ^2 >= 0 ) by QUIN_1:def 1, XREAL_1:63;
A19: for x being real number holds Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)

proof

let x be real number ; :: thesis: Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)
thus Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = (((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((z - y),(y - x))|) * x)) + ((Sum (sqr (S - X))) - (r ^2)) by POLYEQ_1:def 2
.= ((Sum (sqr (T - S))) * (x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A12, A15, A18, QUIN_1:16
.= (Sum (sqr (T - S))) * ((x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))))
.= Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) by POLYEQ_1:def 3 ; :: thesis: verum

end;

then ((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) by A12, POLYEQ_1:11;
then A20: ( ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 ) or ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 ) ) by A16, XREAL_1:133;
A21: (((Sum (sqr (T - S))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2)) + ((2 * |((z - y),(y - x))|) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) - (- ((Sum (sqr (S - X))) - (r ^2))) = (((Sum (sqr (T - S))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2)) + ((2 * |((z - y),(y - x))|) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) + ((Sum (sqr (S - X))) - (r ^2))
.= Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by POLYEQ_1:def 2
.= Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A19
.= (Sum (sqr (T - S))) * (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) by POLYEQ_1:def 3
.= 0 ;
|.(e1 - x).| ^2 = |.((((1 * y) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2 by EUCLID:50
.= |.(((y - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2 by EUCLID:29
.= |.(((y + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) - x).| ^2 by JORDAN2C:7
.= |.((y + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))) - x).| ^2 by EUCLID:45
.= |.((y - x) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))).| ^2 by JORDAN2C:7
.= |.((y - x) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y))).| ^2 by EUCLID:49
.= ((|.(y - x).| ^2) + (2 * |(((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)),(y - x))|)) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2) by EUCLID_2:45
.= ((Sum (sqr (S - X))) + (2 * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * |((z - y),(y - x))|))) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2) by A14, A5, EUCLID_2:19
.= ((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + (((abs (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |.(z - y).|) ^2) by TOPRNS_1:7
.= ((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + (((abs (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) ^2) * (|.(z - y).| ^2))
.= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (|.(z - y).| ^2)) by COMPLEX1:75
.= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (|.(T - S).| ^2)) by A1, A2
.= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S)))) by A6, SQUARE_1:def 2
.= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S))))
.= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S))))
.= ((((Sum (sqr (S - X))) - (r ^2)) + (r ^2)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S))))
.= ((((Sum (sqr (S - X))) - (r ^2)) + (r ^2)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S))))
.= r ^2 by A21 ;
then ( |.(e1 - x).| = r or |.(e1 - x).| = - r ) by SQUARE_1:40;
then A22: e1 in Sphere (x,r) by A17, A13;
A23: (4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2)) < 0 by A12, A15, XREAL_1:129, XREAL_1:132;
then A24: e1 in halfline (y,z) by A12, A18, A20, QUIN_1:25;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ( (halfline (y,z)) /\ (Sphere (x,r)) c= {e1} & e1 = ((1 - a) * y) + (a * z) )

let d be set ; :: thesis: ( d in {e1} implies d in (halfline (y,z)) /\ (Sphere (x,r)) )
assume d in {e1} ; :: thesis: d in (halfline (y,z)) /\ (Sphere (x,r))
then d = e1 by TARSKI:def 1;
hence d in (halfline (y,z)) /\ (Sphere (x,r)) by A24, A22, XBOOLE_0:def 4; :: thesis: verum

end;

A25: z - y = T - S by A1, A2;

hereby :: according to TARSKI:def 3 :: thesis: e1 = ((1 - a) * y) + (a * z)

let d be set ; :: thesis: ( d in (halfline (y,z)) /\ (Sphere (x,r)) implies d in {e1} )
assume A26: d in (halfline (y,z)) /\ (Sphere (x,r)) ; :: thesis: d in {e1}
then d in halfline (y,z) by XBOOLE_0:def 4;
then consider l being real number such that
A27: d = ((1 - l) * y) + (l * z) and
A28: 0 <= l by Th26;
l is Real by XREAL_0:def 1;
then A29: |.(l * (z - y)).| ^2 = ((abs l) * |.(z - y).|) ^2 by TOPRNS_1:7
.= ((abs l) ^2) * (|.(z - y).| ^2)
.= (l ^2) * (|.(z - y).| ^2) by COMPLEX1:75 ;
d in Sphere (x,r) by A26, XBOOLE_0:def 4;
then r = |.((((1 - l) * y) + (l * z)) - x).| by A27, Th9
.= |.((((1 * y) - (l * y)) + (l * z)) - x).| by EUCLID:50
.= |.(((y - (l * y)) + (l * z)) - x).| by EUCLID:29
.= |.((y - ((l * y) - (l * z))) - x).| by EUCLID:47
.= |.((y - x) - ((l * y) - (l * z))).| by JORDAN2C:7
.= |.((y - x) + (- (l * (y - z)))).| by EUCLID:49
.= |.((y - x) + (l * (- (y - z)))).| by EUCLID:40
.= |.((y - x) + (l * (z - y))).| by EUCLID:44 ;
then r ^2 = ((|.(y - x).| ^2) + (2 * |((l * (z - y)),(y - x))|)) + (|.(l * (z - y)).| ^2) by EUCLID_2:45
.= ((|.(y - x).| ^2) + (2 * (l * |((z - y),(y - x))|))) + (|.(l * (z - y)).| ^2) by EUCLID_2:19 ;
then (((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((z - y),(y - x))|) * l)) + ((Sum (sqr (S - X))) - (r ^2)) = 0 by A7, A14, A5, A25, A29;
then Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),l) = 0 by POLYEQ_1:def 2;
then ( l = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ) by A12, A15, A18, POLYEQ_1:5;
hence d in {e1} by A12, A23, A18, A20, A27, A28, QUIN_1:25, TARSKI:def 1; :: thesis: verum

end;

thus e1 = ((1 - a) * y) + (a * z) by A10; :: thesis: verum