theorem Th7: :: JORDAN3:7

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i being Element of NAT st p in LSeg (f,i) holds
Index (p,f) <= i