let i, m, n be 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:15;
(N-bound D) - (S-bound D) >= 0
by SPRECT_1:22, XREAL_1:48;
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:64;
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:6;
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_0:30;
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:52
;
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_0:30;
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:52
;
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, Th3;
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, Th4;
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:15;
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:3;
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_0:30;
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:52
;
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_0:30;
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:52
.=
(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_0:30;
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:52
.=
(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:15;
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:4;
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_0:30;
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:52
;
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,n)proof
let x be
object ;
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 object ; 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:15;
(E-bound D) - (W-bound D) >= 0
by SPRECT_1:21, XREAL_1:48;
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:64;
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:6;
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,n)then 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,n)then 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,n)then 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,n)then 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;