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 ( 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 ) ) ; :: thesis: it1 = it2
then ( it1 <= it2 & it2 <= it1 ) ;
hence it1 = it2 by XXREAL_0:1; :: thesis: verum