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:6;
then i + 1 <= len f by A3, XXREAL_0:2;
then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def 3;
then A8: f /. (i + 1) in LSeg (f,i) by RLTOPSP1:68;
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:70;
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:22;
reconsider v1 = p as Element of REAL 2 by EUCLID:22;
A11: |.(v2 - v1).| > 0 by A10, EUCLID:17;
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:139;
then A16: s0 <= s0 + (r0 / |.(v2 - v1).|) by A11, XREAL_1:29, XREAL_1:139;
A17: r0 / |.(v2 - v1).| > 0 by A15, A11, XREAL_1:139;
then A18: - (r0 / |.(v2 - v1).|) < - 0 by XREAL_1:24;
then A19: (- r0) / |.(v2 - v1).| < 0 by XCMPLX_1:187;
then A20: s0 + 0 > s0 + ((- r0) / |.(v2 - v1).|) by XREAL_1:6;
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:29, XREAL_1:139;
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:6;
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:50;
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:48;
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:10;
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:72;
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:87
.= 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:32
.= (((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:32
.= ((((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:26 ;
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:26
.= ((((((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:26
.= (((((((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 ;
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;
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:33
.= ((((((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:26
.= f /. (i + 1) by A12, A30, EUCLID:33 ;
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:9;
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:187; :: 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:29
.= 1 * q by EUCLID:27
.= q by EUCLID:29 ;
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:42
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) - ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) by EUCLID:38
.= ((((1 - s0) * p) + (s0 * q)) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) by EUCLID:26
.= (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)))) by EUCLID:26
.= ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:26
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:40
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:33
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + ((- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) by EUCLID:40
.= (((- 1) * (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * q) by EUCLID:33
.= ((- (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:40
.= ((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:37
.= (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p by EUCLID:35 ;
then A35: s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) = 0 by A10, EUCLID:34;
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:29
.= 1 * p by EUCLID:27
.= p by EUCLID:29 ;
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:42
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:38
.= ((((1 - s0) * p) + (s0 * q)) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) + (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) by EUCLID:26
.= (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)))) by EUCLID:26
.= ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:26
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:40
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:33
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + ((- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q)) by EUCLID:40
.= (((- 1) * (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * q) by EUCLID:33
.= ((- (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:40
.= (- ((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:37
.= (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p by EUCLID:35 ;
then s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) = 0 by A10, EUCLID:34;
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:22;
A39: |.(v2 - v1).| <> 0 by A10, EUCLID:17;
reconsider u3 = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) as Point of (Euclid 2) by EUCLID:22;
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:6;
reconsider u0 = f /. (i + 1) as Point of (Euclid 2) by EUCLID:22;
A42: q - p = v2 - v1 by EUCLID:69;
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:38
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:26
.= (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:26
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p))) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by EUCLID:40
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by EUCLID:40
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + ((- s0) * q)) by EUCLID:26
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) + (- s0)) * q) by EUCLID:33
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) + (- (1 - s0))) * p) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * q) by EUCLID:33
.= ((- ((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:40
.= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (q - p) by EUCLID:49
.= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (v2 - v1) by A42, EUCLID:65 ;

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:6;
then A45: - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) <= - ((- r0) / |.(v2 - v1).|) by XREAL_1:24;
r0 + r0 = s ;
then A46: r0 < s by A9, XREAL_1:29;
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:22;
A47: - ((- r0) / |.(v2 - v1).|) = (- (- r0)) / |.(v2 - v1).| by XCMPLX_1:187
.= 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:69
.= (abs ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) * |.(v2 - v1).| by A43, EUCLID:11 ;
abs ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) = abs (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) by COMPLEX1:52
.= - (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:64;
then dist (u4,u0) <= r0 by A39, A48, XCMPLX_1:87;
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:65
.= ((- r0) / |.(v2 - v1).|) * (q - p)
.= ((- r0) / |.(v2 - v1).|) * (v2 - v1) by A42, EUCLID:65 ;
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:22;
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:69
.= (abs ((- r0) / |.(v2 - v1).|)) * |.(v2 - v1).| by A49, EUCLID:11
.= ((abs (- r0)) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:67
.= ((abs (- r0)) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= abs (- r0) by A11, XCMPLX_1:87
.= abs r0 by COMPLEX1:52
.= r0 by A9, ABSVALUE:def 1 ;
hence dist (u4,u0) < s by A9, A50, XREAL_1:29; :: 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:17;
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:38
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:26
.= (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:26
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p))) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by EUCLID:40
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by EUCLID:40
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + ((- s0) * q)) by EUCLID:26
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) + (- s0)) * q) by EUCLID:33
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) + (- (1 - s0))) * p) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * q) by EUCLID:33
.= ((- ((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:40
.= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (q - p) by EUCLID:49
.= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1) by A42, EUCLID:65 ;

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:6;
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:48;
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:64;
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:22;
r0 + r0 = s ;
then A56: r0 < s by A9, XREAL_1:29;
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:69
.= |.(((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1)).| by A52
.= (abs ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0)) * |.(v2 - v1).| by EUCLID:11 ;
then dist (u3,u0) <= r0 by A39, A55, XCMPLX_1:87;
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:65
.= (r0 / |.(v2 - v1).|) * (q - p)
.= (r0 / |.(v2 - v1).|) * (v2 - v1) by A42, EUCLID:65 ;
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:22;
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:69
.= (abs (r0 / |.(v2 - v1).|)) * |.(v2 - v1).| by A57, EUCLID:11
.= ((abs r0) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:67
.= ((abs r0) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= abs r0 by A11, XCMPLX_1:87
.= r0 by A9, ABSVALUE:def 1 ;
hence dist (u3,u0) < s by A9, A58, XREAL_1:29; :: 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:17;
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:21;
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;