theorem Th49: :: JORDAN1G:49
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) = mid (f,1,(p .. f))