let a be Real; :: thesis: for r being non negative Real
for r1, r2, s1, s2 being Real
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r be non negative Real; :: thesis: for r1, r2, s1, s2 being Real
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r1, r2, s1, s2 be Real; :: thesis: for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let s, t, o be Point of (TOP-REAL 2); :: thesis: ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) implies HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| )
assume that
A1: s is Point of (Tdisk (o,r)) and
A2: t is Point of (Tdisk (o,r)) and
A3: s <> t and
A4: ( r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) ) and
A5: s1 = (s `1) - (o `1) and
A6: s2 = (s `2) - (o `2) and
A7: a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) ; :: thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(s - o).| <= r by A1, TOPREAL9:8;
then A8: |.(s - o).| ^2 <= r ^2 by SQUARE_1:15;
set C = ((s1 ^2) + (s2 ^2)) - (r ^2);
set A = (r1 ^2) + (r2 ^2);
set M = (s1 * r1) + (s2 * r2);
set B = 2 * ((s1 * r1) + (s2 * r2));
set l1 = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
set l2 = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
A9: delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def 1;
|.(s - o).| ^2 = (((s - o) `1) ^2) + (((s - o) `2) ^2) by JGRAPH_1:29
.= (s1 ^2) + (((s - o) `2) ^2) by A5, TOPREAL3:3
.= (s1 ^2) + (s2 ^2) by A6, TOPREAL3:3 ;
then A10: ((s1 ^2) + (s2 ^2)) - (r ^2) <= (r ^2) - (r ^2) by A8, XREAL_1:9;
then A11: ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) >= 0 ;

A12: now :: thesis: not ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) > ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))

set D = sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))));
assume ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) > ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; :: thesis: contradiction
then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) - (2 * ((s1 * r1) + (s2 * r2))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) - (2 * ((s1 * r1) + (s2 * r2))) by XREAL_1:72;
then - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))) by XREAL_1:9;
then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) by XREAL_1:6;
hence contradiction by A9, A11; :: thesis: verum

end;

( r1 <> 0 or r2 <> 0 ) by A3, A4, TOPREAL3:6;
then A13: 0 + 0 < (r1 ^2) + (r2 ^2) by SQUARE_1:12, XREAL_1:8;
for x being Real holds Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x)

proof

let x be Real; :: thesis: Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x)
thus Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = ((((r1 ^2) + (r2 ^2)) * (x ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * x)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) by POLYEQ_1:def 2
.= (((r1 ^2) + (r2 ^2)) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) by A13, A9, A10, QUIN_1:16
.= ((r1 ^2) + (r2 ^2)) * ((x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))))
.= Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) by POLYEQ_1:def 3 ; :: thesis: verum

end;

then A14: (((s1 ^2) + (s2 ^2)) - (r ^2)) / ((r1 ^2) + (r2 ^2)) = (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) * (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) by A13, POLYEQ_1:11;
delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def 1
.= 4 * ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))) ;
then A15: ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + ((sqrt 4) * (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2))))))) / (2 * ((r1 ^2) + (r2 ^2))) by A10, SQUARE_1:29
.= (2 * (- (((s1 * r1) + (s2 * r2)) - (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))))) / (2 * ((r1 ^2) + (r2 ^2))) by SQUARE_1:20
.= a by A7, XCMPLX_1:91 ;
set H = HC (s,t,o,r);
A16: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A1, A2, A3, Def3;
then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A17: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and
A18: 0 <= l by TOPREAL9:26;
A19: HC (s,t,o,r) = ((1 * s) - (l * s)) + (l * t) by A17, RLVECT_1:35
.= (s - (l * s)) + (l * t) by RLVECT_1:def 8
.= (s + (l * t)) - (l * s) by RLVECT_1:def 3
.= s + ((l * t) - (l * s)) by RLVECT_1:def 3
.= s + (l * (t - s)) by RLVECT_1:34 ;
then A20: (HC (s,t,o,r)) `1 = (s `1) + ((l * (t - s)) `1) by TOPREAL3:2
.= (s `1) + (l * ((t - s) `1)) by TOPREAL3:4
.= (s `1) + (l * ((t `1) - (s `1))) by TOPREAL3:3 ;
HC (s,t,o,r) in Sphere (o,r) by A16, XBOOLE_0:def 4;
then |.((HC (s,t,o,r)) - o).| = r by TOPREAL9:9;
then r ^2 = ((((HC (s,t,o,r)) - o) `1) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by JGRAPH_1:29
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by TOPREAL3:3
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by TOPREAL3:3
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by A17, TOPREAL9:41
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + (((((1 - l) * (s `2)) + (l * (t `2))) - (o `2)) ^2) by A17, TOPREAL9:42
.= ((((l ^2) * ((r1 ^2) + (r2 ^2))) + ((l * 2) * ((s1 * r1) + (s2 * r2)))) + (s1 ^2)) + (s2 ^2) by A4, A5, A6 ;
then ((((r1 ^2) + (r2 ^2)) * (l ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * l)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) = 0 ;
then Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),l) = 0 by POLYEQ_1:def 2;
then A21: ( l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or l = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ) by A13, A9, A10, POLYEQ_1:5;
A22: (HC (s,t,o,r)) `2 = (s `2) + ((l * (t - s)) `2) by A19, TOPREAL3:2
.= (s `2) + (l * ((t - s) `2)) by TOPREAL3:4
.= (s `2) + (l * ((t `2) - (s `2))) by TOPREAL3:3 ;

per cases ( ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 or ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ) by A10;

suppose ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 ; :: thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|

hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A18, A20, A22, A13, A15, A21, A14, A12, EUCLID:53, XREAL_1:141; :: thesis: verum

end;

suppose ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; :: thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|

hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; :: thesis: verum

end;

suppose A23: ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ; :: thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|

now :: thesis: not l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))

A24: now :: thesis: not l = 0

assume l = 0 ; :: thesis: contradiction
then HC (s,t,o,r) = s + (0. (TOP-REAL 2)) by A19, RLVECT_1:10
.= s by RLVECT_1:4 ;
hence contradiction by A1, A2, A3, Def3; :: thesis: verum

end;

assume A25: l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; :: thesis: contradiction

per cases ( 0 < 2 * ((s1 * r1) + (s2 * r2)) or 2 * ((s1 * r1) + (s2 * r2)) <= 0 ) ;

suppose A26: 0 < 2 * ((s1 * r1) + (s2 * r2)) ; :: thesis: contradiction

then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (2 * ((s1 * r1) + (s2 * r2)))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:22;
hence contradiction by A18, A13, A25, A26, XREAL_1:129, XREAL_1:141; :: thesis: verum

end;

suppose 2 * ((s1 * r1) + (s2 * r2)) <= 0 ; :: thesis: contradiction

then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (- (2 * ((s1 * r1) + (s2 * r2))))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:23
.= 0 ;
hence contradiction by A25, A24; :: thesis: verum

end;

end;

end;

hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; :: thesis: verum

end;

end;