:: deftheorem Def3 defines Y-SpanStart JORDAN11:def 3 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for n being Nat st n is_sufficiently_large_for C holds
for b₃ being Element of NAT holds
( b₃ = Y-SpanStart (C,n) iff ( b₃ <= width (Gauge (C,n)) & ( for k being Nat st b₃ <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) & ( for j being Nat st j <= width (Gauge (C,n)) & ( for k being Nat st j <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C ) holds
j >= b₃ ) ) );