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