theorem :: JORDAN5B:29

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))