:: deftheorem Def1 defines Index JORDAN3:def 1 :
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
for b₃ being Element of NAT holds
( b₃ = Index (p,f) iff ex S being non empty Subset of NAT st
( b₃ = min S & S = { i where i is Nat : p in LSeg (f,i) } ) );