:: deftheorem Def3 defines L_Cut JORDAN3:def 3 :
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( ( p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ) & ( not p <> f . ((Index (p,f)) + 1) implies L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) ) );