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