let i, j, m, n be Nat; for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 3 <= i & i < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds
for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ( m <= n & 3 <= i & i < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) implies for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j) )
assume that
A1:
m <= n
and
A2:
3 <= i
and
A3:
i < len (Gauge (E,m))
and
A4:
( 1 < j & j + 1 < width (Gauge (E,m)) )
; for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)
A5:
i - 2 = i -' 2
by A2, XREAL_1:233, XXREAL_0:2;
A6:
2 + 1 <= i
by A2;
then
1 + 1 < i
by NAT_1:13;
then A7:
1 < i - 1
by XREAL_1:20;
A8:
2 |^ (n -' m) > 0
by NEWTON:83;
A9:
i - 3 = i -' 3
by A2, XREAL_1:233;
then
i -' 3 < i -' 2
by A5, XREAL_1:10;
then
(2 |^ (n -' m)) * (i -' 3) < (2 |^ (n -' m)) * (i -' 2)
by A8, XREAL_1:68;
then
((2 |^ (n -' m)) * (i -' 3)) + 1 <= (2 |^ (n -' m)) * (i -' 2)
by NAT_1:13;
then
(2 |^ (n -' m)) * (i -' 3) <= ((2 |^ (n -' m)) * (i -' 2)) -' 1
by NAT_D:55;
then A10:
((2 |^ (n -' m)) * (i -' 3)) + 2 <= (((2 |^ (n -' m)) * (i -' 2)) -' 1) + 2
by XREAL_1:6;
A11:
i -' 1 = i - 1
by A2, XREAL_1:233, XXREAL_0:2;
then A12:
(i -' 1) - 1 = i - (1 + 1)
;
i > 2 + 0
by A6, NAT_1:13;
then
i - 2 > 0
by XREAL_1:20;
then A13:
(2 |^ (n -' m)) * (i -' 2) > 0
by A8, A5, XREAL_1:129;
then
(2 |^ (n -' m)) * (i -' 2) >= 0 + 1
by NAT_1:13;
then A14:
((2 |^ (n -' m)) * ((i -' 1) - 2)) + 2 <= (((2 |^ (n -' m)) * (i -' 2)) + 2) -' 1
by A9, A11, A10, NAT_D:38;
A15:
(i -' 1) + 1 < len (Gauge (E,m))
by A2, A3, XREAL_1:235, XXREAL_0:2;
let i1, j1 be Nat; ( i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 implies cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j) )
assume that
A16:
i1 = ((2 |^ (n -' m)) * (i - 2)) + 2
and
A17:
j1 = ((2 |^ (n -' m)) * (j - 2)) + 2
; cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)
i1 < i1 + 1
by XREAL_1:29;
then A18:
i1 - 1 < i1
by XREAL_1:19;
i1 > 0 + 2
by A16, A5, A13, XREAL_1:6;
then A19:
i1 -' 1 < i1
by A18, XREAL_1:233, XXREAL_0:2;
j - 2 < j - 1
by XREAL_1:10;
then
(2 |^ (n -' m)) * (j - 2) < (2 |^ (n -' m)) * (j - 1)
by A8, XREAL_1:68;
then
j1 < ((2 |^ (n -' m)) * (j - 1)) + 2
by A17, XREAL_1:6;
hence
cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)
by A1, A4, A16, A17, A7, A15, A5, A14, A12, A19, Th47; verum