let j be 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 3;

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:3;
then (f /. j) `1 > p `1 by A9, XXREAL_0:1;
then A10: ((f /. j) `1) - (p `1) > 0 by XREAL_1:50;

now :: thesis: not p `1 < q `1

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:120
.= ((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:2
.= ((1 - a) * ((f /. j) `1)) + ((a * p) `1) by TOPREAL3:4
.= ((1 * ((f /. j) `1)) - (a * ((f /. j) `1))) + (a * (p `1)) by TOPREAL3:4
.= ((f /. j) `1) - (a * (((f /. j) `1) - (p `1)))
.= ((f /. j) `1) - (((f /. j) `1) - (q `1)) by A10, XCMPLX_1:87
.= q `1 ;
(f /. j) `1 >= q `1 by A4, A6, A8, TOPREAL1:3;
then A13: ((f /. j) `1) - (q `1) >= 0 by XREAL_1:48;
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:2
.= ((1 - a) * ((f /. j) `2)) + ((a * p) `2) by TOPREAL3:4
.= ((1 * ((f /. j) `2)) - (a * ((f /. j) `2))) + (a * (p `2)) by TOPREAL3:4
.= q `2 by A4, A5, A8, A14, GOBOARD7:6 ;
then A15: q = ((1 - a) * (f /. j)) + (a * p) by A12, TOPREAL3:6;
assume A16: p `1 < q `1 ; :: thesis: contradiction
then (q `1) - (p `1) > 0 by XREAL_1:50;
then (1 - a) + a >= 0 + a by A10, A11, XREAL_1:7;
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:23;
hence contradiction by A7, A16, JORDAN5C:12, TOPREAL1:25; :: 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:3; :: thesis: verum

end;

end;