theorem Th17: :: JORDAN23:17
for f being FinSequence of (TOP-REAL 2) st 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) = Rev (B_Cut (f,q,p))