theorem :: JORDAN1E:4

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