for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) holds
((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f