theorem Th25: :: JORDAN5C:25

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 f /. i,q, L~ f,f /. 1,f /. (len f)