:: deftheorem Def2 defines Y-InitStart JORDAN11:def 2 :
for C being being_simple_closed_curve Subset of (TOP-REAL 2)
for b₂ being Element of NAT holds
( b₂ = Y-InitStart C iff ( b₂ < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),b₂) c= BDD C & ( for j being Nat st j < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),j) c= BDD C holds
j >= b₂ ) ) );