for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i1 being Nat st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds
(Index (p,f)) + 1 = i1