let m, i, n be Element of NAT ; for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) holds
cell (Gauge D,i),m,n = (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); ( 2 <= m & m + 1 < len (Gauge D,i) & 2 <= n & n + 1 < len (Gauge D,i) implies cell (Gauge D,i),m,n = (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1)) )
set I = Gauge D,i;
set J = Gauge D,(i + 1);
set z = N-bound D;
set e = E-bound D;
set s = S-bound D;
set w = W-bound D;
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)
; cell (Gauge D,i),m,n = (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
A5:
len (Gauge D,(i + 1)) = width (Gauge D,(i + 1))
by JORDAN8:def 1;
A6:
(2 * n) - 3 < (2 * n) - 2
by XREAL_1:17;
(N-bound D) - (S-bound D) >= 0
by SPRECT_1:24, XREAL_1:50;
then
(((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3) <= (((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)
by A6, XREAL_1:66;
then A7:
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3)) <= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2))
by XREAL_1:8;
A8:
m <= m + 1
by NAT_1:11;
A9: ((2 * (n + 1)) -' 2) - 2 =
(((2 * n) + (2 * 1)) -' 2) - 2
.=
(2 * n) - 2
by NAT_D:34
;
A10:
1 <= ((2 * m) -' 2) + 1
by NAT_1:11;
A11:
1 <= len (Gauge D,(i + 1))
by GOBRD11:34;
A12:
1 <= n
by A3, XXREAL_0:2;
then A13:
1 <= (2 * n) -' 1
by Lm12;
(2 * n) -' 1 <= 2 * n
by NAT_D:35;
then A14:
1 <= 2 * n
by A13, XXREAL_0:2;
A15:
((2 * n) -' 1) + 1 = 2 * n
by A12, Lm12, NAT_D:43;
A16:
(2 * n) -' 1 < len (Gauge D,(i + 1))
by A4, Lm15;
then
((2 * n) -' 1) + 1 <= len (Gauge D,(i + 1))
by NAT_1:13;
then
[1,(2 * n)] in Indices (Gauge D,(i + 1))
by A5, A15, A11, A14, MATRIX_1:37;
then A17: ((Gauge D,(i + 1)) * 1,(2 * n)) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2))
by EUCLID:56
;
A18:
(2 * m) -' 1 = (2 * m) - 1
by A1, Lm8, XXREAL_0:2;
A19:
(((2 * m) -' 2) + 1) - 2 = (2 * m) - 3
by A1, Lm14;
A20:
1 <= ((2 * n) -' 2) + 1
by NAT_1:11;
A21:
(2 * m) -' 1 < len (Gauge D,(i + 1))
by A2, Lm15;
A22:
n <= n + 1
by NAT_1:11;
A23:
((2 * n) -' 2) + 1 = (2 * n) -' 1
by A3, Lm9, XXREAL_0:2;
A24: ((2 * (m + 1)) -' 2) - 2 =
(((2 * m) + (2 * 1)) -' 2) - 2
.=
(2 * m) - 2
by NAT_D:34
;
A25:
m < len (Gauge D,i)
by A2, NAT_1:13;
then
m < (2 |^ i) + 3
by JORDAN8:def 1;
then
(2 * m) -' 2 < (2 |^ (i + 1)) + 3
by Lm13;
then A26:
(2 * m) -' 2 < len (Gauge D,(i + 1))
by JORDAN8:def 1;
then
((2 * m) -' 2) + 1 <= len (Gauge D,(i + 1))
by NAT_1:13;
then
[(((2 * m) -' 2) + 1),1] in Indices (Gauge D,(i + 1))
by A5, A11, A10, MATRIX_1:37;
then A27: ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))
by EUCLID:56
;
A28:
1 <= m
by A1, XXREAL_0:2;
then A29:
1 < len (Gauge D,i)
by A25, XXREAL_0:2;
then A30:
((Gauge D,i) * m,1) `1 = ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1
by A1, A25, A11, Th7;
A31:
len (Gauge D,i) = width (Gauge D,i)
by JORDAN8:def 1;
then A32:
n < width (Gauge D,i)
by A4, NAT_1:13;
then A33:
((Gauge D,i) * 1,n) `2 = ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2
by A3, A31, A29, A11, Th8;
A34:
1 <= (2 * m) -' 2
by A1, Lm11;
then A35:
cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1) = { |[r,q]| where r, q is Real : ( ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r & r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1 & ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q & q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2 ) }
by A5, A13, A26, A16, GOBRD11:32;
(2 * m) -' 2 = (2 * m) - 2
by A1, Lm7;
then
(2 * m) -' 2 < (2 * m) -' 1
by A18, XREAL_1:17;
then A36:
((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 < ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1
by A5, A11, A34, A21, GOBOARD5:4;
A37:
(2 * n) -' 1 = (2 * n) - 1
by A3, Lm8, XXREAL_0:2;
A38:
(((2 * n) -' 2) + 1) - 2 = (2 * n) - 3
by A3, Lm14;
n < (2 |^ i) + 3
by A31, A32, JORDAN8:def 1;
then
(2 * n) -' 2 < (2 |^ (i + 1)) + 3
by Lm13;
then A39:
(2 * n) -' 2 < width (Gauge D,(i + 1))
by A5, JORDAN8:def 1;
then
((2 * n) -' 2) + 1 <= len (Gauge D,(i + 1))
by A5, NAT_1:13;
then
[1,(((2 * n) -' 2) + 1)] in Indices (Gauge D,(i + 1))
by A5, A11, A20, MATRIX_1:37;
then A40: ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2))
by EUCLID:56
;
A41:
1 <= (2 * n) -' 2
by A3, Lm11;
then A42:
cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2) = { |[r,q]| where r, q is Real : ( ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r & r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1 & ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q & q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2 ) }
by A34, A26, A39, GOBRD11:32;
A43:
1 <= (2 * m) -' 1
by A28, Lm12;
then A44:
cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2) = { |[r,q]| where r, q is Real : ( ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r & r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1 & ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q & q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2 ) }
by A41, A39, A21, GOBRD11:32;
A45:
cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1) = { |[r,q]| where r, q is Real : ( ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r & r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1 & ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q & q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2 ) }
by A5, A13, A43, A16, A21, GOBRD11:32;
A46:
cell (Gauge D,i),m,n = { |[r,q]| where r, q is Real : ( ((Gauge D,i) * m,1) `1 <= r & r <= ((Gauge D,i) * (m + 1),1) `1 & ((Gauge D,i) * 1,n) `2 <= q & q <= ((Gauge D,i) * 1,(n + 1)) `2 ) }
by A28, A12, A25, A32, GOBRD11:32;
1 <= n + 1
by NAT_1:11;
then
[1,(n + 1)] in Indices (Gauge D,i)
by A4, A31, A29, MATRIX_1:37;
then A47: ((Gauge D,i) * 1,(n + 1)) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2))
by EUCLID:56
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * (n + 1)) -' 2) - 2))
by A3, A22, Lm10, XXREAL_0:2
;
1 <= m + 1
by NAT_1:11;
then
[(m + 1),1] in Indices (Gauge D,i)
by A2, A31, A29, MATRIX_1:37;
then A48: ((Gauge D,i) * (m + 1),1) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (1 - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2))
by EUCLID:56
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * (m + 1)) -' 2) - 2))
by A1, A8, Lm10, XXREAL_0:2
;
(2 * n) -' 2 = (2 * n) - 2
by A3, Lm7;
then
(2 * n) -' 2 < (2 * n) -' 1
by A37, XREAL_1:17;
then A49:
((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 < ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2
by A5, A11, A41, A16, GOBOARD5:5;
A50:
((2 * m) -' 1) + 1 = 2 * m
by A28, Lm12, NAT_D:43;
(2 * m) -' 1 <= 2 * m
by NAT_D:35;
then A51:
1 <= 2 * m
by A43, XXREAL_0:2;
((2 * m) -' 1) + 1 <= len (Gauge D,(i + 1))
by A21, NAT_1:13;
then
[(2 * m),1] in Indices (Gauge D,(i + 1))
by A5, A50, A11, A51, MATRIX_1:37;
then A52: ((Gauge D,(i + 1)) * (2 * m),1) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2))
by EUCLID:56
;
A53:
((2 * m) -' 2) + 1 = (2 * m) -' 1
by A1, Lm9, XXREAL_0:2;
thus
cell (Gauge D,i),m,n c= (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
XBOOLE_0:def 10 (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1)) c= cell (Gauge D,i),m,nproof
let x be
set ;
TARSKI:def 3 ( not x in cell (Gauge D,i),m,n or x in (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1)) )
assume
x in cell (Gauge D,i),
m,
n
;
x in (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
then consider r,
q being
Real such that A54:
x = |[r,q]|
and A55:
((Gauge D,i) * m,1) `1 <= r
and A56:
r <= ((Gauge D,i) * (m + 1),1) `1
and A57:
((Gauge D,i) * 1,n) `2 <= q
and A58:
q <= ((Gauge D,i) * 1,(n + 1)) `2
by A46;
( (
r <= ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 &
q <= ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 ) or (
r >= ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 &
q <= ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 ) or (
r <= ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 &
q >= ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 ) or (
r >= ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 &
q >= ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 ) )
;
then
(
|[r,q]| in cell (Gauge D,(i + 1)),
((2 * m) -' 2),
((2 * n) -' 2) or
|[r,q]| in cell (Gauge D,(i + 1)),
((2 * m) -' 1),
((2 * n) -' 2) or
|[r,q]| in cell (Gauge D,(i + 1)),
((2 * m) -' 2),
((2 * n) -' 1) or
|[r,q]| in cell (Gauge D,(i + 1)),
((2 * m) -' 1),
((2 * n) -' 1) )
by A53, A23, A24, A9, A50, A15, A42, A44, A35, A45, A52, A17, A48, A47, A30, A33, A55, A56, A57, A58;
hence
x in (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
by A54, Lm3;
verum
end;
let x be set ; TARSKI:def 3 ( not x in (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1)) or x in cell (Gauge D,i),m,n )
A59:
(2 * m) - 3 < (2 * m) - 2
by XREAL_1:17;
(E-bound D) - (W-bound D) >= 0
by SPRECT_1:23, XREAL_1:50;
then
(((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3) <= (((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2)
by A59, XREAL_1:66;
then A60:
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3)) <= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2))
by XREAL_1:8;
assume A61:
x in (((cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2)) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1))) \/ (cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1))
; x in cell (Gauge D,i),m,n
per cases
( x in cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2) or x in cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2) or x in cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1) or x in cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1) )
by A61, Lm3;
suppose
x in cell (Gauge D,(i + 1)),
((2 * m) -' 2),
((2 * n) -' 2)
;
x in cell (Gauge D,i),m,nthen consider r,
q being
Real such that A62:
x = |[r,q]|
and A63:
((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r
and A64:
r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1
and A65:
((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q
and A66:
q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2
by A42;
A67:
q <= ((Gauge D,i) * 1,(n + 1)) `2
by A38, A9, A7, A40, A47, A66, XXREAL_0:2;
r <= ((Gauge D,i) * (m + 1),1) `1
by A19, A24, A60, A27, A48, A64, XXREAL_0:2;
hence
x in cell (Gauge D,i),
m,
n
by A46, A30, A33, A62, A63, A65, A67;
verum end; suppose
x in cell (Gauge D,(i + 1)),
((2 * m) -' 1),
((2 * n) -' 2)
;
x in cell (Gauge D,i),m,nthen consider r,
q being
Real such that A68:
x = |[r,q]|
and A69:
((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r
and A70:
r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1
and A71:
((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q
and A72:
q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2
by A44;
A73:
((Gauge D,i) * m,1) `1 <= r
by A30, A36, A69, XXREAL_0:2;
q <= ((Gauge D,i) * 1,(n + 1)) `2
by A38, A9, A7, A40, A47, A72, XXREAL_0:2;
hence
x in cell (Gauge D,i),
m,
n
by A24, A50, A46, A52, A48, A33, A68, A70, A71, A73;
verum end; suppose
x in cell (Gauge D,(i + 1)),
((2 * m) -' 2),
((2 * n) -' 1)
;
x in cell (Gauge D,i),m,nthen consider r,
q being
Real such that A74:
x = |[r,q]|
and A75:
((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r
and A76:
r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1
and A77:
((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q
and A78:
q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2
by A35;
A79:
((Gauge D,i) * 1,n) `2 <= q
by A33, A49, A77, XXREAL_0:2;
r <= ((Gauge D,i) * (m + 1),1) `1
by A19, A24, A60, A27, A48, A76, XXREAL_0:2;
hence
x in cell (Gauge D,i),
m,
n
by A9, A15, A46, A17, A47, A30, A74, A75, A78, A79;
verum end; suppose
x in cell (Gauge D,(i + 1)),
((2 * m) -' 1),
((2 * n) -' 1)
;
x in cell (Gauge D,i),m,nthen consider r,
q being
Real such that A80:
x = |[r,q]|
and A81:
((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r
and A82:
r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1
and A83:
((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q
and A84:
q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2
by A45;
A85:
((Gauge D,i) * 1,n) `2 <= q
by A33, A49, A83, XXREAL_0:2;
((Gauge D,i) * m,1) `1 <= r
by A30, A36, A81, XXREAL_0:2;
hence
x in cell (Gauge D,i),
m,
n
by A24, A9, A50, A15, A46, A52, A17, A48, A47, A80, A82, A84, A85;
verum end;