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 and
A2: f is alternating and
A3: ( 1 <= i & i + 2 <= len f ) and
A4: ( u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q ) and
A5: 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 )
A6: i + (1 + 1) = (i + 1) + 1 ;
i + 1 <= i + 2 by XREAL_1:8;
then A7: i + 1 <= len f by A3, XXREAL_0:2;
A8: 1 <= i + 1 by NAT_1:11;
set p0 = f /. (i + 1);
( LSeg f,i = LSeg (f /. i),(f /. (i + 1)) & LSeg f,(i + 1) = LSeg (f /. (i + 1)),(f /. (i + 2)) ) by A3, A6, A7, A8, TOPREAL1:def 5;
then A9: ( f /. (i + 1) in LSeg f,i & f /. (i + 1) in LSeg f,(i + 1) ) 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 A10: 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 A4, RLTOPSP1:71;
then p in LSeg f,i by A9, 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 A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: 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 r0 = s / 2 as Real ;
A12: r0 > 0 by A10, XREAL_1:141;
reconsider u0 = f /. (i + 1) as Point of (Euclid 2) by EUCLID:25;
reconsider v1 = p as Element of REAL 2 by EUCLID:25;
reconsider v2 = q as Element of REAL 2 by EUCLID:25;
A13: |.(v2 - v1).| > 0 by A11, EUCLID:20;
then A14: r0 / |.(v2 - v1).| > 0 by A12, XREAL_1:141;
then A15: - (r0 / |.(v2 - v1).|) < - 0 by XREAL_1:26;
consider s0 being Real such that
A16: ( f /. (i + 1) = ((1 - s0) * p) + (s0 * q) & 0 <= s0 & s0 <= 1 ) by A4;
set r3 = min (s0 + (r0 / |.(v2 - v1).|)),1;
set r4 = max (s0 + ((- r0) / |.(v2 - v1).|)),0 ;
A17: |.(v2 - v1).| <> 0 by A11, EUCLID:20;
A18: (- r0) / |.(v2 - v1).| < 0 by A15, XCMPLX_1:188;
set p3 = ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q);
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;
A19: s0 < s0 + (r0 / |.(v2 - v1).|) by A14, XREAL_1:31;
A20: s0 <= s0 + (r0 / |.(v2 - v1).|) by A14, XREAL_1:31;
then ( 0 <= min (s0 + (r0 / |.(v2 - v1).|)),1 & min (s0 + (r0 / |.(v2 - v1).|)),1 <= 1 ) by A16, XXREAL_0:20, XXREAL_0:22;
then A21: ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) in LSeg p,q ;
V: q - p = v2 - v1 by EUCLID:73;
A22: (((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 A16, 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 V, EUCLID:69 ;

now

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

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

then A23: min (s0 + (r0 / |.(v2 - v1).|)),1 = 1 by XXREAL_0:def 9;
min (s0 + (r0 / |.(v2 - v1).|)),1 <= s0 + (r0 / |.(v2 - v1).|) by XXREAL_0:17;
then A24: (min (s0 + (r0 / |.(v2 - v1).|)),1) + (- s0) <= (s0 + (r0 / |.(v2 - v1).|)) + (- s0) by XREAL_1:8;
(min (s0 + (r0 / |.(v2 - v1).|)),1) - s0 >= 0 by A16, A23, XREAL_1:50;
then abs ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) <= r0 / |.(v2 - v1).| by A24, ABSVALUE:def 1;
then A25: (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;
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 A22
.= (abs ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0)) * |.(v2 - v1).| by EUCLID:14 ;
then A26: dist u3,u0 <= r0 by A17, A25, XCMPLX_1:88;
r0 + r0 = s ;
then r0 < s by A10, XREAL_1:31;
hence dist u3,u0 < s by A26, XXREAL_0:2; :: thesis: verum

end;

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

then U: (((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 A22, XXREAL_0:def 9
.= ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (q - p) by V, EUCLID:69
.= (r0 / |.(v2 - v1).|) * (q - p)
.= (r0 / |.(v2 - v1).|) * (v2 - v1) by V, 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;
A27: 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 U, 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 A13, XCMPLX_1:88
.= r0 by A12, ABSVALUE:def 1 ;
r0 + r0 = s ;
hence dist u3,u0 < s by A10, A27, XREAL_1:31; :: thesis: verum

end;

end;

end;

then u3 in { u6 where u6 is Point of (Euclid 2) : dist u0,u6 < s } ;
then A28: ((1 - (min (s0 + (r0 / |.(v2 - v1).|)),1)) * p) + ((min (s0 + (r0 / |.(v2 - v1).|)),1) * q) in Ball u0,s by METRIC_1:18;
set p4 = ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q);
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;
A29: s0 + 0 > s0 + ((- r0) / |.(v2 - v1).|) by A18, XREAL_1:8;
then A30: s0 + ((- r0) / |.(v2 - v1).|) <= 1 by A16, 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 A31: ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) in LSeg p,q ;
A32: (((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 A16, 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 V, 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 A33: 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 A34: - ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) <= - ((- r0) / |.(v2 - v1).|) by XREAL_1:26;
A35: - ((- r0) / |.(v2 - v1).|) = (- (- r0)) / |.(v2 - v1).| by XCMPLX_1:188
.= r0 / |.(v2 - v1).| ;
abs ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0) = abs (- ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) by COMPLEX1:138
.= - (0 - s0) by A16, A33, ABSVALUE:def 1 ;
then A36: (abs ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) - s0)) * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A33, A34, A35, XREAL_1:66;
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;
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 A32, EUCLID:14 ;
then A37: dist u4,u0 <= r0 by A17, A36, XCMPLX_1:88;
r0 + r0 = s ;
then r0 < s by A10, XREAL_1:31;
hence dist u4,u0 < s by A37, XXREAL_0:2; :: thesis: verum

end;

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

then U: (((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 A32, XXREAL_0:def 10
.= ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (q - p) by V, EUCLID:69
.= ((- r0) / |.(v2 - v1).|) * (q - p)
.= ((- r0) / |.(v2 - v1).|) * (v2 - v1) by V, 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;
A38: 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 U, 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 A13, XCMPLX_1:88
.= abs r0 by COMPLEX1:138
.= r0 by A12, ABSVALUE:def 1 ;
r0 + r0 = s ;
hence dist u4,u0 < s by A10, A38, XREAL_1:31; :: thesis: verum

end;

end;

end;

then u4 in { u7 where u7 is Point of (Euclid 2) : dist u0,u7 < s } ;
then A39: ((1 - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) * p) + ((max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) * q) in Ball u0,s by METRIC_1:18;
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

assume A40: 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
A41: 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

A42: max (s0 + ((- r0) / |.(v2 - v1).|)),0 <= 1 by A30, XXREAL_0:28;
s0 + ((- r0) / |.(v2 - v1).|) < s0 + (r0 / |.(v2 - v1).|) by A14, A18, XREAL_1:8;
then A43: max (s0 + ((- r0) / |.(v2 - v1).|)),0 < s0 + (r0 / |.(v2 - v1).|) by A16, A19, XXREAL_0:29;

per cases ( max (s0 + ((- r0) / |.(v2 - v1).|)),0 < 1 or max (s0 + ((- r0) / |.(v2 - v1).|)),0 = 1 ) by A42, 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 A43, XXREAL_0:21;
then A44: (min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 ) > 0 by XREAL_1:52;
min (s0 + (r0 / |.(v2 - v1).|)),1 >= s0 by A16, A20, XXREAL_0:20;
then (min (s0 + (r0 / |.(v2 - v1).|)),1) - s0 >= 0 by XREAL_1:50;
then A45: ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) >= 0 by A44;
set r5 = ((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 <= s0 by A16, A29, 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 A44, XREAL_1:74;
then A46: ((min (s0 + (r0 / |.(v2 - v1).|)),1) - s0) / ((min (s0 + (r0 / |.(v2 - v1).|)),1) - (max (s0 + ((- r0) / |.(v2 - v1).|)),0 )) <= 1 by A44, XCMPLX_1:60;
A47: ((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 A44, 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 A16, A47, 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 A45, A46; :: 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 A16, 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 A15, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

A48: f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1)) by A1, A2, A3, Th59;

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 A40, A41, A48, Def1;

suppose A49: 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 A16, EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33 ;
hence contradiction by A4; :: thesis: verum

end;

suppose s0 <> 1 ; :: thesis: contradiction

then A50: 1 > s0 by A16, XXREAL_0:1;
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 A16, A49, 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 s0 + (- (min (s0 + (r0 / |.(v2 - v1).|)),1)) = 0 by A11, EUCLID:38;
hence contradiction by A19, A50, XXREAL_0:21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A51: 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 A16, EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33 ;
hence contradiction by A5, A9, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A52: 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 A16, A51, 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 A11, EUCLID:38;
hence contradiction by A16, A29, A52, XXREAL_0:29; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

then consider x being set such that
A53: ( 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;
A54: 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 A21, A31, TOPREAL1:12;
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 A28, A39, 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, A53, A54; :: thesis: verum

end;

end;