theorem Th13: :: JORDAN3:13
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds
i1 = (Index (p,f)) + 1