let it1, it2 be Element of NAT ; :: thesis: ( it1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) c= BDD C & ( for j being Element of 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 >= it1 ) & it2 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it2) c= BDD C & ( for j being Element of 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 >= it2 ) implies it1 = it2 )
assume that
A3: it1 < width (Gauge (C,(ApproxIndex C))) and
A4: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) c= BDD C and
A5: for j being Element of 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 >= it1 and
A6: it2 < width (Gauge (C,(ApproxIndex C))) and
A7: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it2) c= BDD C and
A8: for j being Element of 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 >= it2 ; :: thesis: it1 = it2
A9: it2 <= it1 by A3, A4, A8;
it1 <= it2 by A5, A6, A7;
hence it1 = it2 by A9, XXREAL_0:1; :: thesis: verum