for f being FinSequence of (TOP-REAL 2) st f is unfolded & f is weakly-one-to-one holds
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) is unfolded