let m, i, n be Element of NAT ; :: thesis:
let D be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
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) ; :: thesis:
A5: len (Gauge D,i) = width (Gauge D,i) by JORDAN8:def 1;
A6: len (Gauge D,(i + 1)) = width (Gauge D,(i + 1)) by JORDAN8:def 1;
A7: ( 1 <= m & 1 <= n ) by A1, A3, XXREAL_0:2;
A8: ((2 * m) -' 2) + 1 = (2 * m) -' 1 by A1, Lm9, XXREAL_0:2;
A9: ((2 * n) -' 2) + 1 = (2 * n) -' 1 by A3, Lm9, XXREAL_0:2;
A10: (2 * m) -' 2 = (2 * m) - 2 by A1, Lm7;
A11: (2 * m) -' 1 = (2 * m) - 1 by A1, Lm8, XXREAL_0:2;
A12: (2 * n) -' 2 = (2 * n) - 2 by A3, Lm7;
A13: (2 * n) -' 1 = (2 * n) - 1 by A3, Lm8, XXREAL_0:2;
A14: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 by A1, Lm14;
A15: (((2 * n) -' 2) + 1) - 2 = (2 * n) - 3 by A3, Lm14;
A16: ((2 * (m + 1)) -' 2) - 2 = (((2 * m) + (2 * 1)) -' 2) - 2
.= (2 * m) - 2 by NAT_D:34 ;
A17: ((2 * (n + 1)) -' 2) - 2 = (((2 * n) + (2 * 1)) -' 2) - 2
.= (2 * n) - 2 by NAT_D:34 ;
A18: 1 <= (2 * n) -' 1 by A7, Lm12;
A19: 1 <= (2 * m) -' 1 by A7, Lm12;
then A20: ((2 * m) -' 1) + 1 = 2 * m by NAT_D:43;
A21: ((2 * n) -' 1) + 1 = 2 * n by A18, NAT_D:43;
A22: ( m < len (Gauge D,i) & n < width (Gauge D,i) ) by A2, A4, A5, NAT_1:13;
then A23: 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 A7, GOBRD11:32;
A24: 1 < len (Gauge D,i) by A7, A22, XXREAL_0:2;
A25: 1 <= len (Gauge D,(i + 1)) by GOBRD11:34;
A26: ( 1 <= (2 * m) -' 2 & 1 <= (2 * n) -' 2 ) by A1, A3, Lm11;
A27: ( (2 * m) -' 2 < (2 * m) -' 1 & (2 * n) -' 2 < (2 * n) -' 1 ) by A10, A11, A12, A13, XREAL_1:17;
m < (2 |^ i) + 3 by A22, JORDAN8:def 1;
then (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then A28: (2 * m) -' 2 < len (Gauge D,(i + 1)) by JORDAN8:def 1;
n < (2 |^ i) + 3 by A5, A22, JORDAN8:def 1;
then (2 * n) -' 2 < (2 |^ (i + 1)) + 3 by Lm13;
then A29: (2 * n) -' 2 < width (Gauge D,(i + 1)) by A6, JORDAN8:def 1;
then A30: 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 A26, A28, GOBRD11:32;
A31: (2 * n) -' 1 < len (Gauge D,(i + 1)) by A4, Lm15;
A32: (2 * m) -' 1 < len (Gauge D,(i + 1)) by A2, Lm15;
then A33: 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 A19, A26, A29, GOBRD11:32;
A34: 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 A6, A18, A26, A28, A31, GOBRD11:32;
A35: 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 A6, A18, A19, A31, A32, GOBRD11:32;
(E-bound D) - (W-bound D) >= 0 by SPRECT_1:23, XREAL_1:50;
then A36: ((E-bound D) - (W-bound D)) / (2 |^ (i + 1)) >= 0 ;
(2 * m) - 3 < (2 * m) - 2 by XREAL_1:17;
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 A36, XREAL_1:66;
then A37: (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;
(N-bound D) - (S-bound D) >= 0 by SPRECT_1:24, XREAL_1:50;
then A38: ((N-bound D) - (S-bound D)) / (2 |^ (i + 1)) >= 0 ;
(2 * n) - 3 < (2 * n) - 2 by XREAL_1:17;
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 A38, XREAL_1:66;
then A39: (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;
A40: ((2 * m) -' 2) + 1 <= len (Gauge D,(i + 1)) by A28, NAT_1:13;
1 <= ((2 * m) -' 2) + 1 by NAT_1:11;
then [(((2 * m) -' 2) + 1),1] in Indices (Gauge D,(i + 1)) by A6, A25, A40, MATRIX_1:37;
then A41: ((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 ;
(2 * m) -' 1 <= 2 * m by NAT_D:35;
then A42: 1 <= 2 * m by A19, XXREAL_0:2;
(2 * n) -' 1 <= 2 * n by NAT_D:35;
then A43: 1 <= 2 * n by A18, XXREAL_0:2;
((2 * m) -' 1) + 1 <= len (Gauge D,(i + 1)) by A32, NAT_1:13;
then [(2 * m),1] in Indices (Gauge D,(i + 1)) by A6, A20, A25, A42, MATRIX_1:37;
then A44: ((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 ;
((2 * n) -' 1) + 1 <= len (Gauge D,(i + 1)) by A31, NAT_1:13;
then [1,(2 * n)] in Indices (Gauge D,(i + 1)) by A6, A21, A25, A43, MATRIX_1:37;
then A45: ((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 ;
A46: ((2 * n) -' 2) + 1 <= len (Gauge D,(i + 1)) by A6, A29, NAT_1:13;
1 <= ((2 * n) -' 2) + 1 by NAT_1:11;
then [1,(((2 * n) -' 2) + 1)] in Indices (Gauge D,(i + 1)) by A6, A25, A46, MATRIX_1:37;
then A47: ((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 ;
A48: m <= m + 1 by NAT_1:11;
A49: n <= n + 1 by NAT_1:11;
1 <= m + 1 by NAT_1:11;
then [(m + 1),1] in Indices (Gauge D,i) by A2, A5, A24, MATRIX_1:37;
then A50: ((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, A48, Lm10, XXREAL_0:2 ;
1 <= n + 1 by NAT_1:11;
then [1,(n + 1)] in Indices (Gauge D,i) by A4, A5, A24, MATRIX_1:37;
then A51: ((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, A49, Lm10, XXREAL_0:2 ;
A52: ((Gauge D,i) * m,1) `1 = ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 by A1, A22, A24, A25, Th7;
A53: ((Gauge D,i) * 1,n) `2 = ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 by A3, A5, A22, A24, A25, Th8;
A54: ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 < ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 by A6, A25, A26, A27, A32, GOBOARD5:4;
A55: ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 < ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 by A6, A25, A26, A27, A31, GOBOARD5:5;
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)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in cell (Gauge D,i),m,n ; :: thesis:
then consider r, q being Real such that
A56: x = |[r,q]| and
A57: ( ((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 A23;
( ( 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 A8, A9, A16, A17, A20, A21, A30, A33, A34, A35, A44, A45, A50, A51, A52, A53, A57;
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 A56, Lm3; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A58: 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)) ; :: thesis:

per cases by A58, Lm3;

suppose x in cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 2) ; :: thesis:

then consider r, q being Real such that
A59: x = |[r,q]| and
A60: ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r and
A61: r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1 and
A62: ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q and
A63: q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2 by A30;
A64: r <= ((Gauge D,i) * (m + 1),1) `1 by A14, A16, A37, A41, A50, A61, XXREAL_0:2;
q <= ((Gauge D,i) * 1,(n + 1)) `2 by A15, A17, A39, A47, A51, A63, XXREAL_0:2;
hence x in cell (Gauge D,i),m,n by A23, A52, A53, A59, A60, A62, A64; :: thesis:

end;

suppose x in cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 2) ; :: thesis:

then consider r, q being Real such that
A65: x = |[r,q]| and
A66: ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r and
A67: r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1 and
A68: ((Gauge D,(i + 1)) * 1,((2 * n) -' 2)) `2 <= q and
A69: q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 2) + 1)) `2 by A33;
A70: ((Gauge D,i) * m,1) `1 <= r by A52, A54, A66, XXREAL_0:2;
q <= ((Gauge D,i) * 1,(n + 1)) `2 by A15, A17, A39, A47, A51, A69, XXREAL_0:2;
hence x in cell (Gauge D,i),m,n by A16, A20, A23, A44, A50, A53, A65, A67, A68, A70; :: thesis:

end;

suppose x in cell (Gauge D,(i + 1)),((2 * m) -' 2),((2 * n) -' 1) ; :: thesis:

then consider r, q being Real such that
A71: x = |[r,q]| and
A72: ((Gauge D,(i + 1)) * ((2 * m) -' 2),1) `1 <= r and
A73: r <= ((Gauge D,(i + 1)) * (((2 * m) -' 2) + 1),1) `1 and
A74: ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q and
A75: q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2 by A34;
A76: r <= ((Gauge D,i) * (m + 1),1) `1 by A14, A16, A37, A41, A50, A73, XXREAL_0:2;
((Gauge D,i) * 1,n) `2 <= q by A53, A55, A74, XXREAL_0:2;
hence x in cell (Gauge D,i),m,n by A17, A21, A23, A45, A51, A52, A71, A72, A75, A76; :: thesis:

end;

suppose x in cell (Gauge D,(i + 1)),((2 * m) -' 1),((2 * n) -' 1) ; :: thesis:

then consider r, q being Real such that
A77: x = |[r,q]| and
A78: ((Gauge D,(i + 1)) * ((2 * m) -' 1),1) `1 <= r and
A79: r <= ((Gauge D,(i + 1)) * (((2 * m) -' 1) + 1),1) `1 and
A80: ((Gauge D,(i + 1)) * 1,((2 * n) -' 1)) `2 <= q and
A81: q <= ((Gauge D,(i + 1)) * 1,(((2 * n) -' 1) + 1)) `2 by A35;
A82: ((Gauge D,i) * m,1) `1 <= r by A52, A54, A78, XXREAL_0:2;
((Gauge D,i) * 1,n) `2 <= q by A53, A55, A80, XXREAL_0:2;
hence x in cell (Gauge D,i),m,n by A16, A17, A20, A21, A23, A44, A45, A50, A51, A77, A79, A81, A82; :: thesis:

end;