let it1, it2 be Element of NAT ; ( it1 < width (Gauge (C,(ApproxIndex C))) & cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) 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 >= 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 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
A5:
it1 < width (Gauge (C,(ApproxIndex C)))
and
A6:
cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it1) c= BDD C
and
A7:
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 >= it1
and
A8:
it2 < width (Gauge (C,(ApproxIndex C)))
and
A9:
cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),it2) c= BDD C
and
A10:
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 >= it2
; it1 = it2
A11:
it2 <= it1
by A5, A6, A10;
it1 <= it2
by A7, A8, A9;
hence
it1 = it2
by A11, XXREAL_0:1; verum