theorem Th5: :: JORDAN1E:5

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 holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))