let i, j, m, n be Nat; for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds
for i1, j1 being Nat st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds
cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j)
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ( m <= n & 1 < i & i + 1 < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) implies for i1, j1 being Nat st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds
cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j) )
set G = Gauge (E,m);
set G1 = Gauge (E,n);
assume that
A1:
m <= n
and
A2:
1 < i
and
A3:
i + 1 < len (Gauge (E,m))
and
A4:
1 < j
and
A5:
j + 1 < width (Gauge (E,m))
; for i1, j1 being Nat st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds
cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j)
set i2 = ((2 |^ (n -' m)) * (i -' 2)) + 2;
set j2 = ((2 |^ (n -' m)) * (j -' 2)) + 2;
set i3 = ((2 |^ (n -' m)) * (i -' 1)) + 2;
set j3 = ((2 |^ (n -' m)) * (j -' 1)) + 2;
let i1, j1 be Nat; ( ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 implies cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j) )
assume that
A6:
((2 |^ (n -' m)) * (i - 2)) + 2 <= i1
and
A7:
i1 < ((2 |^ (n -' m)) * (i - 1)) + 2
and
A8:
((2 |^ (n -' m)) * (j - 2)) + 2 <= j1
and
A9:
j1 < ((2 |^ (n -' m)) * (j - 1)) + 2
; cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j)
A10:
j - 1 = j -' 1
by A4, XREAL_1:233;
then A11:
((2 |^ (n -' m)) * (j -' 1)) + 2 <= width (Gauge (E,n))
by A1, A4, A5, Th35;
A12:
1 + 1 <= i
by A2, NAT_1:13;
then A13:
((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2
by XREAL_1:233;
i < i + 1
by XREAL_1:29;
then A14:
i < len (Gauge (E,m))
by A3, XXREAL_0:2;
then A15:
1 <= ((2 |^ (n -' m)) * (i - 2)) + 2
by A1, A2, Th31;
then A16:
1 <= i1
by A6, XXREAL_0:2;
j1 + 1 <= ((2 |^ (n -' m)) * (j -' 1)) + 2
by A9, A10, NAT_1:13;
then A17:
( j1 + 1 < ((2 |^ (n -' m)) * (j -' 1)) + 2 or j1 + 1 = ((2 |^ (n -' m)) * (j -' 1)) + 2 )
by XXREAL_0:1;
let e be object ; TARSKI:def 3 ( not e in cell ((Gauge (E,n)),i1,j1) or e in cell ((Gauge (E,m)),i,j) )
assume A18:
e in cell ((Gauge (E,n)),i1,j1)
; e in cell ((Gauge (E,m)),i,j)
then reconsider p = e as Point of (TOP-REAL 2) ;
((2 |^ (n -' m)) * (i - 1)) + 2 <= len (Gauge (E,n))
by A1, A2, A3, Th34;
then A19:
i1 < len (Gauge (E,n))
by A7, XXREAL_0:2;
then A20:
i1 + 1 <= len (Gauge (E,n))
by NAT_1:13;
A21: (j + 1) - (1 + 1) =
j - 1
.=
j -' 1
by A4, XREAL_1:233
;
1 < j + 1
by A4, XREAL_1:29;
then A22:
(Gauge (E,m)) * (i,(j + 1)) = (Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 1)) + 2))
by A1, A2, A5, A14, A21, A13, Th33;
A23:
i - 1 = i -' 1
by A2, XREAL_1:233;
then A24:
((2 |^ (n -' m)) * (i -' 1)) + 2 <= len (Gauge (E,n))
by A1, A2, A3, Th34;
i1 + 1 <= ((2 |^ (n -' m)) * (i -' 1)) + 2
by A7, A23, NAT_1:13;
then A25:
( i1 + 1 < ((2 |^ (n -' m)) * (i -' 1)) + 2 or i1 + 1 = ((2 |^ (n -' m)) * (i -' 1)) + 2 )
by XXREAL_0:1;
A26:
((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2
by A12, XREAL_1:233;
A27: (i + 1) - (1 + 1) =
i - 1
.=
i -' 1
by A2, XREAL_1:233
;
A28:
((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2
by A12, XREAL_1:233;
then A29:
((2 |^ (n -' m)) * (i -' 2)) + 2 <= len (Gauge (E,n))
by A6, A19, XXREAL_0:2;
j < j + 1
by XREAL_1:29;
then A30:
j < width (Gauge (E,m))
by A5, XXREAL_0:2;
then A31:
1 <= ((2 |^ (n -' m)) * (j - 2)) + 2
by A1, A4, Th32;
then A32:
1 <= j1
by A8, XXREAL_0:2;
then
1 < j1 + 1
by NAT_1:13;
then A33:
((Gauge (E,n)) * (i1,(j1 + 1))) `2 <= ((Gauge (E,n)) * (i1,(((2 |^ (n -' m)) * (j -' 1)) + 2))) `2
by A19, A16, A11, A17, GOBOARD5:4;
((2 |^ (n -' m)) * (j - 1)) + 2 <= width (Gauge (E,n))
by A1, A4, A5, Th35;
then A34:
j1 < width (Gauge (E,n))
by A9, XXREAL_0:2;
then A35:
j1 + 1 <= width (Gauge (E,n))
by NAT_1:13;
then A36:
((Gauge (E,n)) * (i1,j1)) `1 <= p `1
by A18, A20, A16, A32, JORDAN9:17;
A37:
1 + 1 <= j
by A4, NAT_1:13;
then A38:
((2 |^ (n -' m)) * (j -' 2)) + 2 = ((2 |^ (n -' m)) * (j - 2)) + 2
by XREAL_1:233;
then
( ((2 |^ (n -' m)) * (j -' 2)) + 2 < j1 or ((2 |^ (n -' m)) * (j -' 2)) + 2 = j1 )
by A8, XXREAL_0:1;
then A39:
((Gauge (E,n)) * (i1,(((2 |^ (n -' m)) * (j -' 2)) + 2))) `2 <= ((Gauge (E,n)) * (i1,j1)) `2
by A19, A34, A16, A31, A38, GOBOARD5:4;
A40:
((2 |^ (n -' m)) * (j -' 2)) + 2 = ((2 |^ (n -' m)) * (j - 2)) + 2
by A37, XREAL_1:233;
then A41:
(Gauge (E,m)) * (i,j) = (Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2))
by A1, A2, A4, A14, A30, A28, Th33;
1 < i + 1
by A2, XREAL_1:29;
then A42:
(Gauge (E,m)) * ((i + 1),j) = (Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 1)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2))
by A1, A3, A4, A30, A27, A38, Th33;
A43:
p `1 <= ((Gauge (E,n)) * ((i1 + 1),j1)) `1
by A18, A20, A35, A16, A32, JORDAN9:17;
1 < i1 + 1
by A16, NAT_1:13;
then A44:
((Gauge (E,n)) * ((i1 + 1),j1)) `1 <= ((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 1)) + 2),j1)) `1
by A34, A32, A24, A25, GOBOARD5:3;
A45:
((Gauge (E,n)) * (i1,j1)) `2 <= p `2
by A18, A20, A35, A16, A32, JORDAN9:17;
A46:
((2 |^ (n -' m)) * (j -' 2)) + 2 <= width (Gauge (E,n))
by A8, A34, A40, XXREAL_0:2;
then ((Gauge (E,n)) * (i1,(((2 |^ (n -' m)) * (j -' 2)) + 2))) `2 =
((Gauge (E,n)) * (1,(((2 |^ (n -' m)) * (j -' 2)) + 2))) `2
by A19, A16, A31, A38, GOBOARD5:1
.=
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2))) `2
by A15, A31, A29, A46, A26, A38, GOBOARD5:1
;
then A47:
((Gauge (E,m)) * (i,j)) `2 <= p `2
by A45, A41, A39, XXREAL_0:2;
A48:
p `2 <= ((Gauge (E,n)) * (i1,(j1 + 1))) `2
by A18, A20, A35, A16, A32, JORDAN9:17;
A49:
1 < ((2 |^ (n -' m)) * (j -' 1)) + 2
by A9, A32, A10, XXREAL_0:2;
then ((Gauge (E,n)) * (i1,(((2 |^ (n -' m)) * (j -' 1)) + 2))) `2 =
((Gauge (E,n)) * (1,(((2 |^ (n -' m)) * (j -' 1)) + 2))) `2
by A19, A16, A11, GOBOARD5:1
.=
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 1)) + 2))) `2
by A15, A29, A13, A11, A49, GOBOARD5:1
;
then A50:
p `2 <= ((Gauge (E,m)) * (i,(j + 1))) `2
by A48, A22, A33, XXREAL_0:2;
( ((2 |^ (n -' m)) * (i -' 2)) + 2 < i1 or ((2 |^ (n -' m)) * (i -' 2)) + 2 = i1 )
by A6, A28, XXREAL_0:1;
then A51:
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),j1)) `1 <= ((Gauge (E,n)) * (i1,j1)) `1
by A19, A34, A15, A32, A28, GOBOARD5:3;
A52:
1 < ((2 |^ (n -' m)) * (i -' 1)) + 2
by A7, A16, A23, XXREAL_0:2;
then ((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 1)) + 2),j1)) `1 =
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 1)) + 2),1)) `1
by A34, A32, A24, GOBOARD5:2
.=
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 1)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2))) `1
by A31, A46, A38, A24, A52, GOBOARD5:2
;
then A53:
p `1 <= ((Gauge (E,m)) * ((i + 1),j)) `1
by A43, A42, A44, XXREAL_0:2;
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),j1)) `1 =
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),1)) `1
by A34, A15, A32, A28, A29, GOBOARD5:2
.=
((Gauge (E,n)) * ((((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2))) `1
by A15, A31, A28, A40, A29, A46, GOBOARD5:2
;
then
((Gauge (E,m)) * (i,j)) `1 <= p `1
by A36, A41, A51, XXREAL_0:2;
hence
e in cell ((Gauge (E,m)),i,j)
by A2, A3, A4, A5, A53, A47, A50, JORDAN9:17; verum