theorem Th23: :: JORDAN3:23

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