theorem Th3: :: JORDAN1B:3

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st 1 <= len f & p in L~ f holds
(R_Cut (f,p)) . 1 = f . 1