let i be Element of NAT ; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2)
for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q & not p in (LSeg f,i) \/ (LSeg f,(i + 1)) holds
for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2)
for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q & not p in (LSeg f,i) \/ (LSeg f,(i + 1)) holds
for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )
let p, q be Point of (TOP-REAL 2); :: thesis: for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q & not p in (LSeg f,i) \/ (LSeg f,(i + 1)) holds
for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )
let u be Point of (Euclid 2); :: thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q & not p in (LSeg f,i) \/ (LSeg f,(i + 1)) implies for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s ) )
assume that
A1: ( f is special & f is alternating ) and
A2: 1 <= i and
A3: i + 2 <= len f and
A4: u = f /. (i + 1) and
A5: f /. (i + 1) in LSeg p,q and
A6: f /. (i + 1) <> q and
A7: not p in (LSeg f,i) \/ (LSeg f,(i + 1)) ; :: thesis: for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )
set p0 = f /. (i + 1);
i + 1 <= i + 2 by XREAL_1:8;
then i + 1 <= len f by A3, XXREAL_0:2;
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, TOPREAL1:def 5;
then A8: f /. (i + 1) in LSeg f,i by RLTOPSP1:69;
let s be Real; :: thesis: ( s > 0 implies ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s ) )
assume A9: s > 0 ; :: thesis: ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )

per cases ( p = q or p <> q ) ;

suppose p = q ; :: thesis: ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )

then f /. (i + 1) in {p} by A5, RLTOPSP1:71;
then p in LSeg f,i by A8, TARSKI:def 1;
hence ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s ) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A10: p <> q ; :: thesis: ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )

reconsider v2 = q as Element of REAL 2 by EUCLID:25;
reconsider v1 = p as Element of REAL 2 by EUCLID:25;
A11: |.(v2 - v1).| > 0 by A10, EUCLID:20;
reconsider r0 = s / 2 as Real ;
consider s0 being Real such that
A12: f /. (i + 1) = ((1 - s0) * p) + (s0 * q) and
A13: 0 <= s0 and
A14: s0 <= 1 by A5;
set r3 = min (s0 + (r0 / |.(v2 - v1).|)),1;
set r4 = max (s0 + ((- r0) / |.(v2 - v1).|)),0 ;
set p4 = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q);
set p3 = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q);
A15: r0 > 0 by A9, XREAL_1:141;
then A16: s0 <= s0 + (r0 / |.(v2 - v1).|) by A11, XREAL_1:31, XREAL_1:141;
A17: r0 / |.(v2 - v1).| > 0 by A15, A11, XREAL_1:141;
then A18: - (r0 / |.(v2 - v1).|) < - 0 by XREAL_1:26;
then A19: (- r0) / |.(v2 - v1).| < 0 by XCMPLX_1:188;
then A20: s0 + 0 > s0 + ((- r0) / |.(v2 - v1).|) by XREAL_1:8;
then A21: s0 + ((- r0) / |.(v2 - v1).|) <= 1 by A14, XXREAL_0:2;
then ( 0 <= max (s0 + ((- r0) / |.(v2 - v1).|)),0 & max (s0 + ((- r0) / |.(v2 - v1).|)),0 <= 1 ) by XXREAL_0:28, XXREAL_0:30;
then A22: ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) in LSeg p,q ;
A23: s0 < s0 + (r0 / |.(v2 - v1).|) by A15, A11, XREAL_1:31, XREAL_1:141;
not LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) c= (LSeg f,i) \/ (LSeg f,(i + 1))

proof

A24: f /. (i + 1) in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))

proof

s0 + ((- r0) / |.(v2 - v1).|) < s0 + (r0 / |.(v2 - v1).|) by A9, A19, XREAL_1:8;
then A25: max (s0 + ((- r0) / |.(v2 - v1).|)),0 < s0 + (r0 / |.(v2 - v1).|) by A17, A13, XXREAL_0:29;
A26: max (s0 + ((- r0) / |.(v2 - v1).|)),0 <= 1 by A21, XXREAL_0:28;

per cases ( max (s0 + ((- r0) / |.(v2 - v1).|)),0 < 1 or max (s0 + ((- r0) / |.(v2 - v1).|)),0 = 1 ) by A26, XXREAL_0:1;

suppose max (s0 + ((- r0) / |.(v2 - v1).|)),0 < 1 ; :: thesis: f /. (i + 1) in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))

then max (s0 + ((- r0) / |.(v2 - v1).|)),0 < min (s0 + (r0 / |.(v2 - v1).|)),1 by A25, XXREAL_0:21;
then A27: (min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) > 0 by XREAL_1:52;
set r5 = ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ));
min (s0 + (r0 / |.(v2 - v1).|)),1 >= s0 by A14, A16, XXREAL_0:20;
then A28: (min (s0 + (r0 / |.(v2 - v1).|)),1) - s0 >= 0 by XREAL_1:50;
max (s0 + ((- r0) / |.(v2 - v1).|)),0 <= s0 by A13, A20, XXREAL_0:28;
then (min (s0 + (r0 / |.(v2 - v1).|)),1) - s0 <= (min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) by XREAL_1:12;
then ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) <= ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) by A27, XREAL_1:74;
then A29: ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) <= 1 by A27, XCMPLX_1:60;
A30: ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (min (s0 + (r0 / |.(v2 - v1).|)),1)) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) = (min (s0 + (r0 / |.(v2 - v1).|)),1) - ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))
.= (min (s0 + (r0 / |.(v2 - v1).|)),1) - ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) by A27, XCMPLX_1:88
.= s0 ;
((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) = (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:36
.= (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + (((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:36
.= ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:30 ;
then ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) = (((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:30
.= ((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p))) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:30
.= (((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p))) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:34 ;
then ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) = (((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:34
.= (((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:34 ;
then ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) = (((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + (((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q) by EUCLID:34;
then ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + ((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) = (((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + (((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + (((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q) by EUCLID:37
.= ((((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) + ((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((((1 - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )))) * (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q) + (((((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q)) by EUCLID:30
.= f /. (i + 1) by A12, A30, EUCLID:37 ;
hence f /. (i + 1) in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by A27, A28, A29; :: thesis: verum

end;

suppose max (s0 + ((- r0) / |.(v2 - v1).|)),0 = 1 ; :: thesis: f /. (i + 1) in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))

then ( s0 + ((- r0) / |.(v2 - v1).|) = 1 or 0 = 1 ) by XXREAL_0:16;
then (s0 + ((- r0) / |.(v2 - v1).|)) - s0 >= s0 - s0 by A14, XREAL_1:11;
hence f /. (i + 1) in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by A18, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

A31: f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1)) by A1, A2, A3, Th59;
assume A32: LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) c= (LSeg f,i) \/ (LSeg f,(i + 1)) ; :: thesis: contradiction

per cases ( f /. (i + 1) = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) or f /. (i + 1) = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) ) by A32, A24, A31, Def1;

suppose A33: f /. (i + 1) = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) ; :: thesis: contradiction

now

per cases ( s0 = 1 or s0 <> 1 ) ;

suppose s0 = 1 ; :: thesis: contradiction

then f /. (i + 1) = (0. (TOP-REAL 2)) + (1 * q) by A12, EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33 ;
hence contradiction by A6; :: thesis: verum

end;

suppose A34: s0 <> 1 ; :: thesis: contradiction

0. (TOP-REAL 2) = (((1 - s0) * p) + (s0 * q)) - (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) by A12, A33, EUCLID:46
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) - ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) by EUCLID:42
.= ((((1 - s0) * p) + (s0 * q)) + (- ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) + (- ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) by EUCLID:30
.= (- ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)))) by EUCLID:30
.= ((- ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) by EUCLID:30
.= (((- (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) by EUCLID:44
.= (((- (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) + (1 - s0)) * p) + ((s0 * q) + (- ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q))) by EUCLID:37
.= (((- (1 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) + (1 - s0)) * p) + ((s0 * q) + ((- (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q)) by EUCLID:44
.= (((- 1) * (s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((s0 + (- (min (s0 + (r0 / |.(v2 - v1).|)),1))) * q) by EUCLID:37
.= ((- (s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((s0 + (- (min (s0 + (r0 / |.(v2 - v1).|)),1))) * q)
.= (- ((s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) + ((s0 + (- (min (s0 + (r0 / |.(v2 - v1).|)),1))) * q) by EUCLID:44
.= ((s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q) - ((s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) ;
then (s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * q = - (- ((s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p)) by EUCLID:41
.= (s0 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p by EUCLID:39 ;
then A35: s0 + (- (min (s0 + (r0 / |.(v2 - v1).|)),1)) = 0 by A10, EUCLID:38;
1 > s0 by A14, A34, XXREAL_0:1;
hence contradiction by A23, A35, XXREAL_0:21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A36: f /. (i + 1) = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) ; :: thesis: contradiction

now

per cases ( s0 = 0 or s0 <> 0 ) ;

suppose s0 = 0 ; :: thesis: contradiction

then f /. (i + 1) = (1 * p) + (0. (TOP-REAL 2)) by A12, EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33 ;
hence contradiction by A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A37: s0 <> 0 ; :: thesis: contradiction

0. (TOP-REAL 2) = (((1 - s0) * p) + (s0 * q)) - (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by A12, A36, EUCLID:46
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) - ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) by EUCLID:42
.= ((((1 - s0) * p) + (s0 * q)) + (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) + (- ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) by EUCLID:30
.= (- ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)))) by EUCLID:30
.= ((- ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:30
.= (((- (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:44
.= (((- (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) + (1 - s0)) * p) + ((s0 * q) + (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q))) by EUCLID:37
.= (((- (1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) + (1 - s0)) * p) + ((s0 * q) + ((- (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q)) by EUCLID:44
.= (((- 1) * (s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + ((s0 + (- (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * q) by EUCLID:37
.= ((- (s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ))) * p) + ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q)
.= (- ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q) by EUCLID:44
.= (- ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) + ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q)
.= ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q) + (- ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p))
.= ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q) - ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) ;
then (s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * q = - (- ((s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p)) by EUCLID:41
.= (s0 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p by EUCLID:39 ;
then s0 + (- (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) = 0 by A10, EUCLID:38;
hence contradiction by A13, A20, A37, XXREAL_0:29; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

then A38: ex x being set st
( x in LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) & not x in (LSeg f,i) \/ (LSeg f,(i + 1)) ) by TARSKI:def 3;
reconsider u4 = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) as Point of (Euclid 2) by EUCLID:25;
A39: |.(v2 - v1).| <> 0 by A10, EUCLID:20;
reconsider u3 = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) as Point of (Euclid 2) by EUCLID:25;
A40: min (s0 + (r0 / |.(v2 - v1).|)),1 <= 1 by XXREAL_0:22;
0 <= min (s0 + (r0 / |.(v2 - v1).|)),1 by A9, A13, XXREAL_0:20;
then ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) in LSeg p,q by A40;
then A41: LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) c= LSeg p,q by A22, TOPREAL1:12;
reconsider u0 = f /. (i + 1) as Point of (Euclid 2) by EUCLID:25;
A42: q - p = v2 - v1 by EUCLID:73;
A43: (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) - (f /. (i + 1)) = (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) + ((- ((1 - s0) * p)) - (s0 * q)) by A12, EUCLID:42
.= ((((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:30
.= (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) + (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:30
.= ((((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + (- ((1 - s0) * p))) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) + ((- s0) * q) by EUCLID:44
.= ((((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((- (1 - s0)) * p)) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) + ((- s0) * q) by EUCLID:44
.= (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((- (1 - s0)) * p)) + (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) + ((- s0) * q)) by EUCLID:30
.= (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((- (1 - s0)) * p)) + (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) + (- s0)) * q) by EUCLID:37
.= (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) + (- (1 - s0))) * p) + (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * q) by EUCLID:37
.= ((- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) * p) + (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * q)
.= (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * q) - (((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * p) by EUCLID:44
.= ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * (q - p) by EUCLID:53
.= ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) * (v2 - v1) by A42, EUCLID:69 ;

now

per cases ( s0 + ((- r0) / |.(v2 - v1).|) <= 0 or not s0 + ((- r0) / |.(v2 - v1).|) <= 0 ) ;

suppose s0 + ((- r0) / |.(v2 - v1).|) <= 0 ; :: thesis: dist u4,u0 < s

then A44: max (s0 + ((- r0) / |.(v2 - v1).|)),0 = 0 by XXREAL_0:def 10;
max (s0 + ((- r0) / |.(v2 - v1).|)),0 >= s0 + ((- r0) / |.(v2 - v1).|) by XXREAL_0:25;
then (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) + (- s0) >= (s0 + ((- r0) / |.(v2 - v1).|)) + (- s0) by XREAL_1:8;
then A45: - ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) <= - ((- r0) / |.(v2 - v1).|) by XREAL_1:26;
r0 + r0 = s ;
then A46: r0 < s by A9, XREAL_1:31;
reconsider v3 = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:25;
A47: - ((- r0) / |.(v2 - v1).|) = (- (- r0)) / |.(v2 - v1).| by XCMPLX_1:188
.= r0 / |.(v2 - v1).| ;
A48: dist u4,u0 = |.(v3 - v4).| by Th20
.= |.((((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) - (f /. (i + 1))).| by EUCLID:73
.= (abs ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) * |.(v2 - v1).| by A43, EUCLID:14 ;
abs ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) = abs (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) by COMPLEX1:138
.= - (0 - s0) by A13, A44, ABSVALUE:def 1 ;
then (abs ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A44, A45, A47, XREAL_1:66;
then dist u4,u0 <= r0 by A39, A48, XCMPLX_1:88;
hence dist u4,u0 < s by A46, XXREAL_0:2; :: thesis: verum

end;

suppose not s0 + ((- r0) / |.(v2 - v1).|) <= 0 ; :: thesis: dist u4,u0 < s

then A49: (((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) - (f /. (i + 1)) = ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (v2 - v1) by A43, XXREAL_0:def 10
.= ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (q - p) by A42, EUCLID:69
.= ((- r0) / |.(v2 - v1).|) * (q - p)
.= ((- r0) / |.(v2 - v1).|) * (v2 - v1) by A42, EUCLID:69 ;
reconsider v3 = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:25;
A50: r0 + r0 = s ;
dist u4,u0 = |.(v3 - v4).| by Th20
.= |.((((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) - (f /. (i + 1))).| by EUCLID:73
.= (abs ((- r0) / |.(v2 - v1).|)) * |.(v2 - v1).| by A49, EUCLID:14
.= ((abs (- r0)) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:153
.= ((abs (- r0)) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= abs (- r0) by A11, XCMPLX_1:88
.= abs r0 by COMPLEX1:138
.= r0 by A9, ABSVALUE:def 1 ;
hence dist u4,u0 < s by A9, A50, XREAL_1:31; :: thesis: verum

end;

end;

end;

then u4 in { u7 where u7 is Point of (Euclid 2) : dist u0,u7 < s } ;
then A51: ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) in Ball u0,s by METRIC_1:18;
A52: (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) - (f /. (i + 1)) = (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) + ((- ((1 - s0) * p)) - (s0 * q)) by A12, EUCLID:42
.= ((((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:30
.= (((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) + (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:30
.= ((((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + (- ((1 - s0) * p))) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) + ((- s0) * q) by EUCLID:44
.= ((((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((- (1 - s0)) * p)) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) + ((- s0) * q) by EUCLID:44
.= (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((- (1 - s0)) * p)) + (((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) + ((- s0) * q)) by EUCLID:30
.= (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((- (1 - s0)) * p)) + (((min (s0 + (r0 / |.(v2 - v1).|)),1) + (- s0)) * q) by EUCLID:37
.= (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) + (- (1 - s0))) * p) + (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * q) by EUCLID:37
.= ((- ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0)) * p) + (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * q)
.= (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * q) - (((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * p) by EUCLID:44
.= ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * (q - p) by EUCLID:53
.= ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * (v2 - v1) by A42, EUCLID:69 ;

now

per cases ( 1 <= s0 + (r0 / |.(v2 - v1).|) or not 1 <= s0 + (r0 / |.(v2 - v1).|) ) ;

suppose A53: 1 <= s0 + (r0 / |.(v2 - v1).|) ; :: thesis: dist u3,u0 < s

min (s0 + (r0 / |.(v2 - v1).|)),1 <= s0 + (r0 / |.(v2 - v1).|) by XXREAL_0:17;
then A54: (min (s0 + (r0 / |.(v2 - v1).|)),1) + (- s0) <= (s0 + (r0 / |.(v2 - v1).|)) + (- s0) by XREAL_1:8;
min (s0 + (r0 / |.(v2 - v1).|)),1 = 1 by A53, XXREAL_0:def 9;
then (min (s0 + (r0 / |.(v2 - v1).|)),1) - s0 >= 0 by A14, XREAL_1:50;
then abs ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) <= r0 / |.(v2 - v1).| by A54, ABSVALUE:def 1;
then A55: (abs ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0)) * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by XREAL_1:66;
reconsider v3 = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:25;
r0 + r0 = s ;
then A56: r0 < s by A9, XREAL_1:31;
dist u3,u0 = |.(v3 - v4).| by Th20
.= |.((((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) - (f /. (i + 1))).| by EUCLID:73
.= |.(((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) * (v2 - v1)).| by A52
.= (abs ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0)) * |.(v2 - v1).| by EUCLID:14 ;
then dist u3,u0 <= r0 by A39, A55, XCMPLX_1:88;
hence dist u3,u0 < s by A56, XXREAL_0:2; :: thesis: verum

end;

suppose not 1 <= s0 + (r0 / |.(v2 - v1).|) ; :: thesis: dist u3,u0 < s

then A57: (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) - (f /. (i + 1)) = ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (v2 - v1) by A52, XXREAL_0:def 9
.= ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (q - p) by A42, EUCLID:69
.= (r0 / |.(v2 - v1).|) * (q - p)
.= (r0 / |.(v2 - v1).|) * (v2 - v1) by A42, EUCLID:69 ;
reconsider v3 = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:25;
A58: r0 + r0 = s ;
dist u3,u0 = |.(v3 - v4).| by Th20
.= |.((((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)) - (f /. (i + 1))).| by EUCLID:73
.= (abs (r0 / |.(v2 - v1).|)) * |.(v2 - v1).| by A57, EUCLID:14
.= ((abs r0) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:153
.= ((abs r0) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= abs r0 by A11, XCMPLX_1:88
.= r0 by A9, ABSVALUE:def 1 ;
hence dist u3,u0 < s by A9, A58, XREAL_1:31; :: thesis: verum

end;

end;

end;

then u3 in { u6 where u6 is Point of (Euclid 2) : dist u0,u6 < s } ;
then ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) in Ball u0,s by METRIC_1:18;
then LSeg (((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q)),(((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q)) c= Ball u0,s by A51, TOPREAL3:28;
hence ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s ) by A4, A38, A41; :: thesis: verum

end;

end;