theorem Th6: :: JORDAN20:6

for j being Nat
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