let m, i, n be Element of NAT ; :: thesis: for D being compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) holds
cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for k being Element of NAT st 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) holds
cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
let k be Element of NAT ; :: thesis: ( 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) implies cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } )
assume that
A1: 2 <= m and
A2: m + 1 < len (Gauge D,i) and
A3: 2 <= n and
A4: n + 1 < len (Gauge D,i) ; :: thesis: cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) }
deffunc H₁( Element of NAT ) -> set = { (cell (Gauge D,(i + $1)),a,b) where a, b is Element of NAT : ( (((2 |^ $1) * m) - (2 |^ ($1 + 1))) + 2 <= a & a <= (((2 |^ $1) * m) - (2 |^ $1)) + 1 & (((2 |^ $1) * n) - (2 |^ ($1 + 1))) + 2 <= b & b <= (((2 |^ $1) * n) - (2 |^ $1)) + 1 ) } ;
defpred S₁[ Element of NAT ] means cell (Gauge D,i),m,n = union H₁($1);
A5: S₁[ 0 ]

proof

A6: now

let m be Element of NAT ; :: thesis: ( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 = m & (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = m )
A7: (2 |^ 0 ) * m = 1 * m by NEWTON:9;
hence (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 = (m - 2) + 2 by NEWTON:10
.= m ;
:: thesis: (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = m
thus (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = (m - 1) + 1 by A7, NEWTON:9
.= m ; :: thesis: verum

end;

H₁( 0 ) = {(cell (Gauge D,i),m,n)}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(cell (Gauge D,i),m,n)} c= H₁( 0 )

let x be set ; :: thesis: ( x in H₁( 0 ) implies x in {(cell (Gauge D,i),m,n)} )
assume x in H₁( 0 ) ; :: thesis: x in {(cell (Gauge D,i),m,n)}
then consider a, b being Element of NAT such that
A8: x = cell (Gauge D,(i + 0 )),a,b and
A9: ( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 & (((2 |^ 0 ) * n) - (2 |^ (0 + 1))) + 2 <= b & b <= (((2 |^ 0 ) * n) - (2 |^ 0 )) + 1 ) ;

now

let a, m be Element of NAT ; :: thesis: ( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 implies a = m )
assume A10: ( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 ) ; :: thesis: a = m
( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 = m & (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 = m ) by A6;
hence a = m by A10, XXREAL_0:1; :: thesis: verum

end;

then ( a = m & b = n ) by A9;
hence x in {(cell (Gauge D,i),m,n)} by A8, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(cell (Gauge D,i),m,n)} or x in H₁( 0 ) )
assume x in {(cell (Gauge D,i),m,n)} ; :: thesis: x in H₁( 0 )
then A11: x = cell (Gauge D,(i + 0 )),m,n by TARSKI:def 1;
( (((2 |^ 0 ) * m) - (2 |^ (0 + 1))) + 2 <= m & m <= (((2 |^ 0 ) * m) - (2 |^ 0 )) + 1 & (((2 |^ 0 ) * n) - (2 |^ (0 + 1))) + 2 <= n & n <= (((2 |^ 0 ) * n) - (2 |^ 0 )) + 1 ) by A6;
hence x in H₁( 0 ) by A11; :: thesis: verum

end;

hence S₁[ 0 ] by ZFMISC_1:31; :: thesis: verum

end;

A12: for w being Element of NAT st S₁[w] holds
S₁[w + 1]

proof

let w be Element of NAT ; :: thesis: ( S₁[w] implies S₁[w + 1] )
assume A13: S₁[w] ; :: thesis: S₁[w + 1]
A14: (i + w) + 1 = i + (w + 1) ;
A15: len (Gauge D,(i + w)) = (2 |^ (i + w)) + 3 by JORDAN8:def 1;
A16: len (Gauge D,i) = (2 |^ i) + 3 by JORDAN8:def 1;
for x being set st x in H₁(w) holds
ex K being set st
( K c= H₁(w + 1) & x c= union K )

proof

let x be set ; :: thesis: ( x in H₁(w) implies ex K being set st
( K c= H₁(w + 1) & x c= union K ) )
assume x in H₁(w) ; :: thesis: ex K being set st
( K c= H₁(w + 1) & x c= union K )
then consider a, b being Element of NAT such that
A17: x = cell (Gauge D,(i + w)),a,b and
A18: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a and
A19: a <= (((2 |^ w) * m) - (2 |^ w)) + 1 and
A20: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= b and
A21: b <= (((2 |^ w) * n) - (2 |^ w)) + 1 ;

now

let m be Element of NAT ; :: thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 )
assume 2 <= m ; :: thesis: 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2
then (2 |^ w) * m >= (2 |^ w) * 2 by XREAL_1:66;
then (2 |^ w) * m >= 2 |^ (w + 1) by NEWTON:11;
then 0 <= ((2 |^ w) * m) - (2 |^ (w + 1)) by XREAL_1:50;
hence 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by XREAL_1:8; :: thesis: verum

end;

then A22: ( 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 & 2 <= (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 ) by A1, A3;
then A23: 2 <= a by A18, XXREAL_0:2;
A24: 2 <= b by A20, A22, XXREAL_0:2;
A25: (2 * a) -' 1 = (2 * a) - 1 by A23, Lm8, XXREAL_0:2;
A26: (2 * b) -' 1 = (2 * b) - 1 by A24, Lm8, XXREAL_0:2;
A27: (2 * a) -' 2 = (2 * a) - 2 by A18, A22, Lm7, XXREAL_0:2;
A28: (2 * b) -' 2 = (2 * b) - 2 by A20, A22, Lm7, XXREAL_0:2;
A29: (2 * a) -' 2 < (2 * a) -' 1 by A25, A27, XREAL_1:17;
A30: (2 * b) -' 2 < (2 * b) -' 1 by A26, A28, XREAL_1:17;
take K = {(cell (Gauge D,((i + w) + 1)),((2 * a) -' 2),((2 * b) -' 2)),(cell (Gauge D,((i + w) + 1)),((2 * a) -' 1),((2 * b) -' 2)),(cell (Gauge D,((i + w) + 1)),((2 * a) -' 2),((2 * b) -' 1)),(cell (Gauge D,((i + w) + 1)),((2 * a) -' 1),((2 * b) -' 1))}; :: thesis: ( K c= H₁(w + 1) & x c= union K )

hereby :: according to TARSKI:def 3 :: thesis: x c= union K

let q be set ; :: thesis: ( q in K implies q in H₁(w + 1) )
assume A31: q in K ; :: thesis: q in H₁(w + 1)

A32: now

let a, m be Element of NAT ; :: thesis: ( 2 <= a & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 )
assume A33: 2 <= a ; :: thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 )
assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; :: thesis: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1
then 2 * a <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by XREAL_1:66;
then 2 * a <= (((2 * (2 |^ w)) * m) - (2 * (2 |^ w))) + 2 ;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 * (2 |^ w))) + 2 by NEWTON:11;
then 2 * a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2 by NEWTON:11;
then (2 * a) - 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by XREAL_1:11;
then A34: (2 * a) -' 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by A33, Lm7;
(((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 0 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XREAL_1:8;
hence (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A34, XXREAL_0:2; :: thesis: verum

end;

A35: now

let a, m be Element of NAT ; :: thesis: ( 2 <= a & (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 )
assume A36: 2 <= a ; :: thesis: ( (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 )
assume (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a ; :: thesis: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * a by XREAL_1:66;
then (((2 * (2 |^ w)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a ;
then (((2 |^ (w + 1)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a by NEWTON:11;
then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4 <= 2 * a by NEWTON:11;
then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) - 2 <= (2 * a) - 2 by XREAL_1:11;
hence (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 by A36, Lm7; :: thesis: verum

end;

then A37: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 2 by A18, A23;
A38: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A19, A23, A32;
then ((2 * a) -' 2) + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by INT_1:20;
then A39: (2 * a) -' 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A23, Lm9, XXREAL_0:2;
A40: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 2 by A20, A24, A35;
A41: (2 * b) -' 2 < (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A21, A24, A32;
then ((2 * b) -' 2) + 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by INT_1:20;
then A42: (2 * b) -' 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A24, Lm9, XXREAL_0:2;
A43: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 1 by A29, A37, XXREAL_0:2;
A44: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 1 by A30, A40, XXREAL_0:2;
( q = cell (Gauge D,(i + (w + 1))),((2 * a) -' 2),((2 * b) -' 2) or q = cell (Gauge D,(i + (w + 1))),((2 * a) -' 1),((2 * b) -' 2) or q = cell (Gauge D,(i + (w + 1))),((2 * a) -' 2),((2 * b) -' 1) or q = cell (Gauge D,(i + (w + 1))),((2 * a) -' 1),((2 * b) -' 1) ) by A31, ENUMSET1:def 2;
hence q in H₁(w + 1) by A37, A38, A39, A40, A41, A42, A43, A44; :: thesis: verum

end;

now

let a, m be Element of NAT ; :: thesis: ( m + 1 < len (Gauge D,i) & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge D,(i + w)) )
assume m + 1 < len (Gauge D,i) ; :: thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge D,(i + w)) )
then (m + 1) - 2 < ((2 |^ i) + 3) - 2 by A16, XREAL_1:11;
then m - 1 < (2 |^ i) + (3 - 2) ;
then m - 1 <= (2 |^ i) + 0 by INT_1:20;
then (2 |^ w) * (m - 1) <= (2 |^ w) * (2 |^ i) by XREAL_1:66;
then (2 |^ w) * (m - 1) <= 2 |^ (w + i) by NEWTON:13;
then A45: ((2 |^ w) * (m - 1)) + 3 <= (2 |^ (w + i)) + 3 by XREAL_1:8;
assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; :: thesis: a + 1 < len (Gauge D,(i + w))
then a + 1 <= ((((2 |^ w) * m) - (2 |^ w)) + 1) + 1 by XREAL_1:8;
then a + 1 < (((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) + 1 by XREAL_1:147;
hence a + 1 < len (Gauge D,(i + w)) by A15, A45, XXREAL_0:2; :: thesis: verum

end;

then ( a + 1 < len (Gauge D,(i + w)) & b + 1 < len (Gauge D,(i + w)) ) by A2, A4, A19, A21;
then cell (Gauge D,(i + w)),a,b = (((cell (Gauge D,((i + w) + 1)),((2 * a) -' 2),((2 * b) -' 2)) \/ (cell (Gauge D,((i + w) + 1)),((2 * a) -' 1),((2 * b) -' 2))) \/ (cell (Gauge D,((i + w) + 1)),((2 * a) -' 2),((2 * b) -' 1))) \/ (cell (Gauge D,((i + w) + 1)),((2 * a) -' 1),((2 * b) -' 1)) by A23, A24, Th9;
hence x c= union K by A17, Lm4; :: thesis: verum

end;

hence cell (Gauge D,i),m,n c= union H₁(w + 1) by A13, Th1; :: according to XBOOLE_0:def 10 :: thesis: union H₁(w + 1) c= cell (Gauge D,i),m,n
H₁(w + 1) is_finer_than H₁(w)

proof

let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( not X in H₁(w + 1) or ex b₁ being set st
( b₁ in H₁(w) & X c= b₁ ) )
assume X in H₁(w + 1) ; :: thesis: ex b₁ being set st
( b₁ in H₁(w) & X c= b₁ )
then consider a, b being Element of NAT such that
A46: X = cell (Gauge D,(i + (w + 1))),a,b and
A47: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a and
A48: a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 and
A49: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= b and
A50: b <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 ;

A51: now

let a be even Element of NAT ; :: thesis: 2 * ((a div 2) + 1) = a + 2
A52: ex e being Element of NAT st a = 2 * e by ABIAN:def 2;
thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1)
.= a + 2 by A52, NAT_D:20 ; :: thesis: verum

end;

A53: now

let a be odd Element of NAT ; :: thesis: 2 * ((a div 2) + 1) = a + 1
consider e being Element of NAT such that
A54: a = (2 * e) + 1 by ABIAN:9;
A55: (2 * e) mod 2 = 0 by NAT_D:13;
thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1)
.= (2 * (((2 * e) div 2) + (1 div 2))) + 2 by A54, A55, NAT_D:19
.= (2 * (e + 0 )) + (1 + 1) by Lm1, NAT_D:20
.= a + 1 by A54 ; :: thesis: verum

end;

deffunc H₂( Element of NAT , Element of NAT ) -> Element of K10(the carrier of (TOP-REAL 2)) = cell (Gauge D,((i + w) + 1)),((2 * ((a div 2) + 1)) -' $1),((2 * ((b div 2) + 1)) -' $2);

A56: now

let a, m be Element of NAT ; :: thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 )
assume A57: 2 <= m ; :: thesis: 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2
2 |^ ((w + 1) + 1) = (2 |^ (w + 1)) * (2 |^ 1) by NEWTON:13
.= (2 |^ (w + 1)) * 2 by NEWTON:10 ;
then (2 |^ (w + 1)) * m >= 2 |^ ((w + 1) + 1) by A57, XREAL_1:66;
then 0 <= ((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1)) by XREAL_1:50;
hence 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by XREAL_1:8; :: thesis: verum

end;

then 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by A1;
then A58: 2 <= a by A47, XXREAL_0:2;
2 <= (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 by A3, A56;
then A59: 2 <= b by A49, XXREAL_0:2;
take Y = cell (Gauge D,(i + w)),((a div 2) + 1),((b div 2) + 1); :: thesis: ( Y in H₁(w) & X c= Y )
2 div 2 <= a div 2 by A58, NAT_2:26;
then A60: 1 + 1 <= (a div 2) + 1 by Lm2, XREAL_1:8;

A61: now

let m be Element of NAT ; :: thesis: 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2
thus 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ (w + 1)))) + (2 + 2)
.= (((2 * (2 |^ w)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:11
.= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:11
.= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 ; :: thesis: verum

end;

A62: now

let m be Element of NAT ; :: thesis: 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1
thus 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ w))) + (1 + 1)
.= (((2 * (2 |^ w)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:11
.= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:11
.= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ; :: thesis: verum

end;

A63: now

let a, m be Element of NAT ; :: thesis: ( m + 1 < len (Gauge D,i) & a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge D,(i + w)) )
assume A64: m + 1 < len (Gauge D,i) ; :: thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge D,(i + w)) )
assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; :: thesis: ((a div 2) + 1) + 1 < len (Gauge D,(i + w))
then a + 3 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3 by XREAL_1:8;
then A65: (a + 3) + 0 < (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by XREAL_1:10;
then A66: (a + 3) + 1 <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by INT_1:20;
m + 1 < (2 |^ i) + 3 by A64, JORDAN8:def 1;
then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ;
then 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34;
then (1 / 2) * (2 * m) < (1 / 2) * ((2 |^ (i + 1)) + 3) by XREAL_1:70;
then m < ((1 / 2) * (2 |^ (i + 1))) + ((1 / 2) * 3) ;
then A67: m < (2 |^ i) + ((1 / 2) * 3) by Th2;
(2 |^ i) + (3 / 2) < (2 |^ i) + 2 by XREAL_1:8;
then m < (2 |^ i) + 2 by A67, XXREAL_0:2;
then m + 1 <= (2 |^ i) + 2 by NAT_1:13;
then (m + 1) - 2 <= ((2 |^ i) + 2) - 2 by XREAL_1:11;
then (2 |^ (w + 1)) * (m - 1) <= (2 |^ (w + 1)) * (2 |^ i) by XREAL_1:66;
then ((2 |^ (w + 1)) * (m - 1)) + 5 < ((2 |^ (w + 1)) * (2 |^ i)) + 6 by XREAL_1:10;
then A68: ((2 |^ (w + 1)) * (m - 1)) + 5 < (2 |^ ((w + 1) + i)) + 6 by NEWTON:13;
then A69: (((2 |^ (w + 1)) * (m - 1)) + 1) + (3 + 1) < (2 * (2 |^ (i + w))) + 6 by A14, NEWTON:11;
A70: ((((2 |^ (w + 1)) * (m - 1)) + 1) + 3) + 1 < (2 * (2 |^ (i + w))) + (2 * 3) by A14, A68, NEWTON:11;

now

per cases ( not a is even or a is even ) ;

suppose A71: not a is even ; :: thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3)

2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1)
.= (a + 1) + 2 by A53, A71
.= a + (1 + 2) ;
hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A65, A69, XXREAL_0:2; :: thesis: verum

end;

suppose A72: a is even ; :: thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3)

2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1)
.= (a + 2) + 2 by A51, A72
.= a + (2 + 2) ;
hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A66, A70, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ((a div 2) + 1) + 1 < len (Gauge D,(i + w)) by A15, XREAL_1:66; :: thesis: verum

end;

then A73: ((a div 2) + 1) + 1 < len (Gauge D,(i + w)) by A2, A48;
2 div 2 <= b div 2 by A59, NAT_2:26;
then A74: 1 + 1 <= (b div 2) + 1 by Lm2, XREAL_1:8;
((b div 2) + 1) + 1 < len (Gauge D,(i + w)) by A4, A50, A63;
then A75: Y = ((H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1)) \/ H₂(1,1) by A60, A73, A74, Th9;

A76: now

let m be Element of NAT ; :: thesis: for a being even Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
let a be even Element of NAT ; :: thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 )
assume A77: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; :: thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
A78: 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A61;
((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 <= a + 2 by A77, XREAL_1:8;
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A51, A78;
hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:70; :: thesis: verum

end;

A79: now

let m be Element of NAT ; :: thesis: for a being even Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds
(a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
let a be even Element of NAT ; :: thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 )
assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; :: thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
then A80: a < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XXREAL_0:1;
A81: 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A62;
a + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A80, INT_1:20;
then (a + 1) + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:8;
then a + (1 + 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ;
then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A51, A81;
hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:70; :: thesis: verum

end;

A82: now

let m be Element of NAT ; :: thesis: for a being odd Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds
(((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
let a be odd Element of NAT ; :: thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 )
assume (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; :: thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1
then A83: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 < a by XXREAL_0:1;
A84: 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A61;
((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1 < a + 1 by A83, XREAL_1:8;
then (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) + 1 <= a + 1 by INT_1:20;
then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A53, A84;
hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:70; :: thesis: verum

end;

A85: now

let m be Element of NAT ; :: thesis: for a being odd Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds
(a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
let a be odd Element of NAT ; :: thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 )
assume A86: a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; :: thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1
A87: 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A62;
a + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A86, XREAL_1:8;
then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A53, A87;
hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:70; :: thesis: verum

end;

per cases ( ( not a is even & not b is even ) or ( not a is even & b is even ) or ( a is even & not b is even ) or ( a is even & b is even ) ) ;

suppose A88: ( not a is even & not b is even ) ; :: thesis: ( Y in H₁(w) & X c= Y )

then A89: (2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A53
.= a by NAT_D:34 ;
A90: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A47, A82, A88;
A91: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A48, A85, A88;
A92: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A49, A82, A88;
(b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A50, A85, A88;
hence Y in H₁(w) by A90, A91, A92; :: thesis: X c= Y
(2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A53, A88
.= b by NAT_D:34 ;
hence X c= Y by A46, A75, A89, XBOOLE_1:7; :: thesis: verum

end;

suppose A93: ( not a is even & b is even ) ; :: thesis: ( Y in H₁(w) & X c= Y )

then A94: (2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A53
.= a by NAT_D:34 ;
A95: (2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A51, A93
.= b by NAT_D:34 ;
A96: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A47, A82, A93;
A97: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A48, A85, A93;
A98: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A49, A76, A93;
(b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A50, A79, A93;
hence Y in H₁(w) by A96, A97, A98; :: thesis: X c= Y
A99: H₂(1,2) c= H₂(2,2) \/ H₂(1,2) by XBOOLE_1:7;
H₂(2,2) \/ H₂(1,2) c= (H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1) by XBOOLE_1:7;
then A100: H₂(1,2) c= (H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1) by A99, XBOOLE_1:1;
(H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1) c= Y by A75, XBOOLE_1:7;
hence X c= Y by A46, A94, A95, A100, XBOOLE_1:1; :: thesis: verum

end;

suppose A101: ( a is even & not b is even ) ; :: thesis: ( Y in H₁(w) & X c= Y )

then A102: (2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A51
.= a by NAT_D:34 ;
A103: (2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A53, A101
.= b by NAT_D:34 ;
A104: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A47, A76, A101;
A105: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A48, A79, A101;
A106: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A49, A82, A101;
(b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A50, A85, A101;
hence Y in H₁(w) by A104, A105, A106; :: thesis: X c= Y
A107: H₂(2,1) c= (H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1) by XBOOLE_1:7;
(H₂(2,2) \/ H₂(1,2)) \/ H₂(2,1) c= Y by A75, XBOOLE_1:7;
hence X c= Y by A46, A102, A103, A107, XBOOLE_1:1; :: thesis: verum

end;

suppose A108: ( a is even & b is even ) ; :: thesis: ( Y in H₁(w) & X c= Y )

then A109: (2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A51
.= a by NAT_D:34 ;
A110: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A47, A76, A108;
A111: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A48, A79, A108;
A112: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A49, A76, A108;
(b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A50, A79, A108;
hence Y in H₁(w) by A110, A111, A112; :: thesis: X c= Y
(2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A51, A108
.= b by NAT_D:34 ;
then X c= H₂(2,2) \/ ((H₂(1,2) \/ H₂(2,1)) \/ H₂(1,1)) by A46, A109, XBOOLE_1:7;
then X c= (H₂(2,2) \/ (H₂(1,2) \/ H₂(2,1))) \/ H₂(1,1) by XBOOLE_1:4;
hence X c= Y by A75, XBOOLE_1:4; :: thesis: verum

end;

end;

end;

then A113: union H₁(w + 1) c= union H₁(w) by SETFAM_1:18;
let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in union H₁(w + 1) or d in cell (Gauge D,i),m,n )
assume d in union H₁(w + 1) ; :: thesis: d in cell (Gauge D,i),m,n
hence d in cell (Gauge D,i),m,n by A13, A113; :: thesis: verum

end;

for w being Element of NAT holds S₁[w] from NAT_1:sch 1(A5, A12);
hence cell (Gauge D,i),m,n = union { (cell (Gauge D,(i + k)),a,b) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } ; :: thesis: verum