let it1, it2 be Element of NAT ; :: thesis: ( it1 <= width (Gauge (C,n)) & ( for k being 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 Nat st j <= width (Gauge (C,n)) & ( for k being 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 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 Nat st j <= width (Gauge (C,n)) & ( for k being 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 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 Nat st j <= width (Gauge (C,n)) & ( for i being 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
A18: S₁[it1] and
A19: S₁[it2] ; :: thesis: it1 = it2
A20: it2 <= it1 by A18, A19;
it1 <= it2 by A18, A19;
hence it1 = it2 by A20, XXREAL_0:1; :: thesis: verum