for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p <> f . 1 holds
R_Cut (f,p) is_S-Seq_joining f /. 1,p