theorem :: JORDAN1E:7

for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p