for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds
L~ (B_Cut (f,p,q)) c= L~ f by Lm3;