let it1, it2 be Element of NAT ; :: thesis: ( it1 <= width (Gauge (C,n)) & ( for k being Element of NAT st it1 <= 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 Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of 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 >= it1 ) & it2 <= width (Gauge (C,n)) & ( for k being Element of NAT st it2 <= 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 Element of NAT st j <= width (Gauge (C,n)) & ( for k being Element of 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 >= it2 ) implies it1 = it2 )
defpred S₁[ Element of NAT ] means ( $1 <= width (Gauge (C,n)) & ( for i being Element of NAT st $1 <= i & i <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),i) c= BDD C ) & ( for j being Element of NAT st j <= width (Gauge (C,n)) & ( for i being Element of NAT st j <= i & i <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),i) c= BDD C ) holds
j >= $1 ) );
assume that
A17: S₁[it1] and
A18: S₁[it2] ; :: thesis: it1 = it2
A19: it2 <= it1 by A17, A18;
it1 <= it2 by A17, A18;
hence it1 = it2 by A19, XXREAL_0:1; :: thesis: verum