theorem :: JORDAN3:25

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
( ( p <> f . 1 implies len (R_Cut (f,p)) = (Index (p,f)) + 1 ) & ( p = f . 1 implies len (R_Cut (f,p)) = Index (p,f) ) )