theorem :: JORDAN5C:30

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