let i be 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 RLVECT_1:def 5
.= (((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 RLVECT_1:def 5
.= ((((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 RLVECT_1:def 3 ;
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 RLVECT_1:def 3
.= ((((((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 RLVECT_1:def 3
.= (((((((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 RLVECT_1:def 7 ;
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 RLVECT_1:def 7
.= (((((((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 RLVECT_1:def 7 ;
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 RLVECT_1:def 7;
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 RLVECT_1:def 6
.= ((((((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 RLVECT_1:def 3
.= f /. (i + 1) by A12, A30, RLVECT_1:def 6 ;
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, Th36;
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;

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

now :: thesis: contradiction

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

suppose s0 = 1 ; :: thesis: contradiction

then f /. (i + 1) = (0. (TOP-REAL 2)) + (1 * q) by A12, RLVECT_1:10
.= 1 * q by RLVECT_1:4
.= q by RLVECT_1:def 8 ;
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, RLVECT_1:5
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) - ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) by RLVECT_1:30
.= ((((1 - s0) * p) + (s0 * q)) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) by RLVECT_1:def 3
.= (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)))) by RLVECT_1:def 3
.= ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by RLVECT_1:def 3
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by RLVECT_1:79
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by RLVECT_1:def 6
.= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + ((- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) by RLVECT_1:79
.= (((- 1) * (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * q) by RLVECT_1:def 6
.= ((- (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 RLVECT_1:79
.= ((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 RLVECT_1:6
.= (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p ;
then A35: s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) = 0 by A10, RLVECT_1:36;
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 :: thesis: contradiction

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

suppose s0 = 0 ; :: thesis: contradiction

then f /. (i + 1) = (1 * p) + (0. (TOP-REAL 2)) by A12, RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
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, RLVECT_1:5
.= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by RLVECT_1:30
.= ((((1 - s0) * p) + (s0 * q)) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) + (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) by RLVECT_1:def 3
.= (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)))) by RLVECT_1:def 3
.= ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by RLVECT_1:def 3
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by RLVECT_1:79
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by RLVECT_1:def 6
.= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + ((- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q)) by RLVECT_1:79
.= (((- 1) * (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * q) by RLVECT_1:def 6
.= ((- (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 RLVECT_1:79
.= (- ((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 RLVECT_1:6
.= (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p ;
then s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) = 0 by A10, RLVECT_1:36;
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 object 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))) ) ;
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: (((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, RLVECT_1:30
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by RLVECT_1:def 3
.= (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by RLVECT_1:def 3
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p))) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by RLVECT_1:79
.= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by RLVECT_1:79
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + ((- s0) * q)) by RLVECT_1:def 3
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) + (- s0)) * q) by RLVECT_1:def 6
.= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) + (- (1 - s0))) * p) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * q) by RLVECT_1:def 6
.= ((- ((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 RLVECT_1:79
.= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (q - p) by RLVECT_1:34
.= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (v2 - v1) ;

now :: thesis: dist (u4,u0) < s

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 A43: 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 A44: - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) <= - ((- r0) / |.(v2 - v1).|) by XREAL_1:24;
r0 + r0 = s ;
then A45: 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;
A46: - ((- r0) / |.(v2 - v1).|) = (- (- r0)) / |.(v2 - v1).| by XCMPLX_1:187
.= r0 / |.(v2 - v1).| ;
A47: dist (u4,u0) = |.(v3 - v4).| by Th5
.= |.((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1))).|
.= |.((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0).| * |.(v2 - v1).| by A42, EUCLID:11 ;
|.((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0).| = |.(- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)).| by COMPLEX1:52
.= - (0 - s0) by A13, A43, ABSVALUE:def 1 ;
then |.((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0).| * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A43, A44, A46, XREAL_1:64;
then dist (u4,u0) <= r0 by A39, A47, XCMPLX_1:87;
hence dist (u4,u0) < s by A45, XXREAL_0:2; :: thesis: verum

end;

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

then A48: (((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 A42, XXREAL_0:def 10
.= ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (q - p)
.= ((- r0) / |.(v2 - v1).|) * (q - p)
.= ((- r0) / |.(v2 - v1).|) * (v2 - v1) ;
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;
A49: r0 + r0 = s ;
dist (u4,u0) = |.(v3 - v4).| by Th5
.= |.((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1))).|
.= |.((- r0) / |.(v2 - v1).|).| * |.(v2 - v1).| by A48, EUCLID:11
.= (|.(- r0).| / |.|.(v2 - v1).|.|) * |.(v2 - v1).| by COMPLEX1:67
.= (|.(- r0).| / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= |.(- r0).| by A11, XCMPLX_1:87
.= |.r0.| by COMPLEX1:52
.= r0 by A9, ABSVALUE:def 1 ;
hence dist (u4,u0) < s by A9, A49, XREAL_1:29; :: thesis: verum

end;

end;

end;

then u4 in { u7 where u7 is Point of (Euclid 2) : dist (u0,u7) < s } ;
then A50: ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) in Ball (u0,s) by METRIC_1:17;
A51: (((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, RLVECT_1:30
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by RLVECT_1:def 3
.= (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by RLVECT_1:def 3
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p))) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by RLVECT_1:79
.= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by RLVECT_1:79
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + ((- s0) * q)) by RLVECT_1:def 3
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) + (- s0)) * q) by RLVECT_1:def 6
.= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) + (- (1 - s0))) * p) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * q) by RLVECT_1:def 6
.= ((- ((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 RLVECT_1:79
.= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (q - p) by RLVECT_1:34
.= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1) ;

now :: thesis: dist (u3,u0) < s

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

suppose A52: 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 A53: (min ((s0 + (r0 / |.(v2 - v1).|)),1)) + (- s0) <= (s0 + (r0 / |.(v2 - v1).|)) + (- s0) by XREAL_1:6;
min ((s0 + (r0 / |.(v2 - v1).|)),1) = 1 by A52, XXREAL_0:def 9;
then (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0 >= 0 by A14, XREAL_1:48;
then |.((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0).| <= r0 / |.(v2 - v1).| by A53, ABSVALUE:def 1;
then A54: |.((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 A55: r0 < s by A9, XREAL_1:29;
dist (u3,u0) = |.(v3 - v4).| by Th5
.= |.((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1))).|
.= |.(((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1)).| by A51
.= |.((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0).| * |.(v2 - v1).| by EUCLID:11 ;
then dist (u3,u0) <= r0 by A39, A54, XCMPLX_1:87;
hence dist (u3,u0) < s by A55, XXREAL_0:2; :: thesis: verum

end;

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

then A56: (((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 A51, XXREAL_0:def 9
.= ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (q - p)
.= (r0 / |.(v2 - v1).|) * (q - p)
.= (r0 / |.(v2 - v1).|) * (v2 - v1) ;
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;
A57: r0 + r0 = s ;
dist (u3,u0) = |.(v3 - v4).| by Th5
.= |.((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1))).|
.= |.(r0 / |.(v2 - v1).|).| * |.(v2 - v1).| by A56, EUCLID:11
.= (|.r0.| / |.|.(v2 - v1).|.|) * |.(v2 - v1).| by COMPLEX1:67
.= (|.r0.| / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def 1
.= |.r0.| by A11, XCMPLX_1:87
.= r0 by A9, ABSVALUE:def 1 ;
hence dist (u3,u0) < s by A9, A57, 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 A50, 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;