for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2)
for j being Nat st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds
LE p,q, L~ f,f /. 1,f /. (len f)