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, X be Element of REAL n; :: thesis:
assume that
A1: S = y and
A2: T = z and
A3: X = x ; :: thesis:
set s = y;
set t = z;
A4: |.(y - x).| = sqrt (Sum (sqr (S - X))) by A1, A3, EUCLID:73;
A5: y - x = S - X by A1, A3, EUCLID:73;
A6: Sum (sqr (T - S)) >= 0 by RVSUM_1:116;
then A7: |.(T - S).| ^2 = Sum (sqr (T - S)) by SQUARE_1:def 4;
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:
A11: |.(T - S).| <> 0 by A1, A2, A8, EUCLID:19;

A12: now

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

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:116;
then A14: |.(S - X).| ^2 = Sum (sqr (S - X)) by SQUARE_1:def 4;
|.(y - x).| < r by A9, Th7;
then (sqrt (Sum (sqr (S - X)))) ^2 < r ^2 by A4, SQUARE_1:78;
then A15: (Sum (sqr (S - X))) - (r ^2 ) < 0 by A14, XREAL_1:51;
then A16: ((Sum (sqr (S - X))) - (r ^2 )) / (Sum (sqr (T - S))) < 0 by A12, XREAL_1:143;
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:
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:65;
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:
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:

end;

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

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

end;

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

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

let d be set ; :: thesis:
assume A26: d in (halfline y,z) /\ (Sphere x,r) ; :: thesis:
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:8
.= ((abs l) ^2 ) * (|.(z - y).| ^2 )
.= (l ^2 ) * (|.(z - y).| ^2 ) by COMPLEX1:161 ;
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:54
.= |.(((y - (l * y)) + (l * z)) - x).| by EUCLID:33
.= |.((y - ((l * y) - (l * z))) - x).| by EUCLID:51
.= |.((y - x) - ((l * y) - (l * z))).| by JORDAN2C:9
.= |.((y - x) + (- (l * (y - z)))).| by EUCLID:53
.= |.((y - x) + (l * (- (y - z)))).| by EUCLID:44
.= |.((y - x) + (l * (z - y))).| by EUCLID:48 ;
then r ^2 = ((|.(y - x).| ^2 ) + (2 * |((l * (z - y)),(y - x))|)) + (|.(l * (z - y)).| ^2 ) by EUCLID_2:67
.= ((|.(y - x).| ^2 ) + (2 * (l * |((z - y),(y - x))|))) + (|.(l * (z - y)).| ^2 ) by EUCLID_2:41 ;
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:27, TARSKI:def 1; :: thesis:

end;

thus e1 = ((1 - a) * y) + (a * z) by A10; :: thesis:
reconsider G = x as Point of (Euclid n) by TOPREAL3:13;