theorem Th26: :: JORDAN5C:26

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