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