theorem Th29: :: JORDAN3:29

for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & Index (p,f) < Index (q,f) holds
q in L~ (L_Cut (f,p))