:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b₂ being Element of NAT holds
( b₂ = ApproxIndex C iff ( b₂ is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= b₂ ) ) );