set m = ApproxIndex C;
defpred S₁[ Nat] means ( $1 <= width (Gauge (C,n)) & ( for k being 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:28;
then (Y-InitStart C) + 1 < ((2 |^ (ApproxIndex C)) + 2) + 1 ;
then A4: Y-InitStart C < (2 |^ (ApproxIndex C)) + 2 by XREAL_1:6;
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:64;
then (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ ((n -' (ApproxIndex C)) + (ApproxIndex C)) by NEWTON:8;
then A6: (2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2) <= 2 |^ n by A1, XREAL_1:235;

A7: now :: thesis: for j being Nat st ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C

2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by NAT_D:35, PREPOWER:93;
then A8: (2 |^ ((ApproxIndex C) -' 1)) + 2 <= (2 |^ (ApproxIndex C)) + 2 by XREAL_1:6;
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 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:11;
then A14: 2 + 1 <= X-SpanStart (C,(ApproxIndex C)) by XREAL_1:6;
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:233;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:233
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A1, XREAL_1:235
.= n -' 1 by A1, A13, XREAL_1:233, XXREAL_0:2 ;
then X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by NEWTON:8;
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:48;
hence cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A15; :: 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:6;
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 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 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 >= 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 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 >= min X
let j be Nat; :: thesis: ( 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 ) implies j >= min X )
A17: j in NAT by ORDINAL1:def 12;
assume S₁[j] ; :: thesis: j >= min X
then j in X by A17;
hence j >= min X by XXREAL_2:def 7; :: thesis: verum