for f being FinSequence of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2)
for i being Nat st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)