set m = ApproxIndex C;
defpred S₁[ Element of NAT ] means ( $1 <= width (Gauge C,n) & ( for k being Element of NAT st $1 <= 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 ) );
set X = { i where i is Element of NAT : S₁[i] } ;
set j0 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A2: { i where i is Element of NAT : S₁[i] } is Subset of NAT from DOMAIN_1:sch 7();
A3: (Y-InitStart C) + 1 < width (Gauge C,(ApproxIndex C)) by Th3;
then (Y-InitStart C) + 1 < (2 |^ (ApproxIndex C)) + (2 + 1) by JORDAN1A:49;
then (Y-InitStart C) + 1 < ((2 |^ (ApproxIndex C)) + 2) + 1 ;
then A4: Y-InitStart C < (2 |^ (ApproxIndex C)) + 2 by XREAL_1:8;
A5: 1 < Y-InitStart C by Th2;
then 1 + 1 <= Y-InitStart C by NAT_1:13;
then (Y-InitStart C) -' 2 < 2 |^ (ApproxIndex C) by A4, NAT_D:54;
then (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= (2 |^ (n -' (ApproxIndex C))) * (2 |^ (ApproxIndex C)) by XREAL_1:66;
then (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ ((n -' (ApproxIndex C)) + (ApproxIndex C)) by NEWTON:13;
then A6: (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ n by A1, XREAL_1:237;

A7: now

2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by NAT_D:35, PREPOWER:107;
then A8: (2 |^ ((ApproxIndex C) -' 1)) + 2 <= (2 |^ (ApproxIndex C)) + 2 by XREAL_1:8;
len (Gauge C,(ApproxIndex C)) = (2 |^ (ApproxIndex C)) + (2 + 1) by JORDAN8:def 1
.= ((2 |^ (ApproxIndex C)) + 2) + 1 ;
then A9: X-SpanStart C,(ApproxIndex C) < len (Gauge C,(ApproxIndex C)) by A8, NAT_1:13;
A10: Y-InitStart C >= 1 + 1 by A5, NAT_1:13;
let j be Element of NAT ; :: thesis: ( ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C )
assume that
A11: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j and
A12: j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C
A13: ApproxIndex C >= 1 by Th1;
1 <= 2 |^ ((ApproxIndex C) -' 1) by PREPOWER:19;
then A14: 2 + 1 <= X-SpanStart C,(ApproxIndex C) by XREAL_1:8;
A15: cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),(Y-InitStart C) c= BDD C by Def2;
j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A11, A12, XXREAL_0:1;
then A16: j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by A10, XREAL_1:235;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:235
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A1, XREAL_1:237
.= n -' 1 by A1, A13, XREAL_1:235, XXREAL_0:2 ;
then X-SpanStart C,n = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2 by NEWTON:13;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),(Y-InitStart C) by A1, A3, A14, A9, A16, Th2, JORDAN1A:69;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by A15, XBOOLE_1:1; :: thesis: verum

end;

2 |^ n <= (2 |^ n) + 1 by NAT_1:11;
then (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= (2 |^ n) + 1 by A6, XXREAL_0:2;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= ((2 |^ n) + 1) + 2 by XREAL_1:8;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= (2 |^ n) + (1 + 2) ;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= len (Gauge C,n) by JORDAN8:def 1;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= width (Gauge C,n) by JORDAN8:def 1;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 in { i where i is Element of NAT : S₁[i] } by A7;
then reconsider X = { i where i is Element of NAT : S₁[i] } as non empty Subset of NAT by A2;
take min X ; :: thesis: ( min X <= width (Gauge C,n) & ( for k being Element of NAT st min X <= 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 >= min X ) )
min X in X by XXREAL_2:def 7;
then ex j being Element of NAT st
( j = min X & S₁[j] ) ;
hence S₁[ min X] ; :: thesis: 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 >= min X
let j be Element of NAT ; :: thesis: ( 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 ) implies j >= min X )
assume S₁[j] ; :: thesis: j >= min X
then j in X ;
hence j >= min X by XXREAL_2:def 7; :: thesis: verum