let j be Element of NAT ; :: thesis: for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg f,j & q in LSeg f,j & (f /. j) `2 = (f /. (j + 1)) `2 & (f /. j) `1 < (f /. (j + 1)) `1 & LE p,q, L~ f,f /. 1,f /. (len f) holds
p `1 <= q `1
let f be S-Sequence_in_R2; :: thesis: for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg f,j & q in LSeg f,j & (f /. j) `2 = (f /. (j + 1)) `2 & (f /. j) `1 < (f /. (j + 1)) `1 & LE p,q, L~ f,f /. 1,f /. (len f) holds
p `1 <= q `1
let p, q be Point of (TOP-REAL 2); :: thesis: ( 1 <= j & j < len f & p in LSeg f,j & q in LSeg f,j & (f /. j) `2 = (f /. (j + 1)) `2 & (f /. j) `1 < (f /. (j + 1)) `1 & LE p,q, L~ f,f /. 1,f /. (len f) implies p `1 <= q `1 )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in LSeg f,j and
A4: q in LSeg f,j and
A5: (f /. j) `2 = (f /. (j + 1)) `2 and
A6: (f /. j) `1 < (f /. (j + 1)) `1 and
A7: LE p,q, L~ f,f /. 1,f /. (len f) ; :: thesis: p `1 <= q `1
j + 1 <= len f by A2, NAT_1:13;
then A8: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A1, TOPREAL1:def 5;

per cases ( p `1 <> (f /. j) `1 or p `1 = (f /. j) `1 ) ;

suppose A9: p `1 <> (f /. j) `1 ; :: thesis: p `1 <= q `1

(f /. j) `1 <= p `1 by A3, A6, A8, TOPREAL1:9;
then (f /. j) `1 < p `1 by A9, XXREAL_0:1;
then A10: ((f /. j) `1 ) - (p `1 ) < 0 by XREAL_1:51;

now

reconsider a = (((f /. j) `1 ) - (q `1 )) / (((f /. j) `1 ) - (p `1 )) as Real ;
A11: 1 - a = ((((f /. j) `1 ) - (p `1 )) / (((f /. j) `1 ) - (p `1 ))) - ((((f /. j) `1 ) - (q `1 )) / (((f /. j) `1 ) - (p `1 ))) by A10, XCMPLX_1:60
.= ((((f /. j) `1 ) - (p `1 )) - (((f /. j) `1 ) - (q `1 ))) / (((f /. j) `1 ) - (p `1 )) by XCMPLX_1:121
.= ((q `1 ) - (p `1 )) / (((f /. j) `1 ) - (p `1 )) ;
A12: (((1 - a) * (f /. j)) + (a * p)) `1 = (((1 - a) * (f /. j)) `1 ) + ((a * p) `1 ) by TOPREAL3:7
.= ((1 - a) * ((f /. j) `1 )) + ((a * p) `1 ) by TOPREAL3:9
.= ((1 * ((f /. j) `1 )) - (a * ((f /. j) `1 ))) + (a * (p `1 )) by TOPREAL3:9
.= ((f /. j) `1 ) - (a * (((f /. j) `1 ) - (p `1 )))
.= ((f /. j) `1 ) - (((f /. j) `1 ) - (q `1 )) by A10, XCMPLX_1:88
.= q `1 ;
(f /. j) `1 <= q `1 by A4, A6, A8, TOPREAL1:9;
then A13: ((f /. j) `1 ) - (q `1 ) <= 0 by XREAL_1:49;
A14: p `2 = (f /. j) `2 by A3, A5, A8, GOBOARD7:6;
(((1 - a) * (f /. j)) + (a * p)) `2 = (((1 - a) * (f /. j)) `2 ) + ((a * p) `2 ) by TOPREAL3:7
.= ((1 - a) * ((f /. j) `2 )) + ((a * p) `2 ) by TOPREAL3:9
.= ((1 * ((f /. j) `2 )) - (a * ((f /. j) `2 ))) + (a * (p `2 )) by TOPREAL3:9
.= q `2 by A4, A5, A8, A14, GOBOARD7:6 ;
then A15: q = ((1 - a) * (f /. j)) + (a * p) by A12, TOPREAL3:11;
assume A16: p `1 > q `1 ; :: thesis: contradiction
then (q `1 ) - (p `1 ) < 0 by XREAL_1:51;
then (1 - a) + a >= 0 + a by A10, A11, XREAL_1:9;
then q in LSeg (f /. j),p by A10, A13, A15;
then LE q,p, L~ f,f /. 1,f /. (len f) by A1, A2, A3, SPRECT_3:40;
hence contradiction by A7, A16, JORDAN5C:12, TOPREAL1:31; :: thesis: verum

end;

hence p `1 <= q `1 ; :: thesis: verum

end;

suppose p `1 = (f /. j) `1 ; :: thesis: p `1 <= q `1

hence p `1 <= q `1 by A4, A6, A8, TOPREAL1:9; :: thesis: verum

end;

end;