let m, n, i, j be Element of NAT ; :: thesis: 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 Element of 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); :: thesis: ( m <= n & 3 <= i & i < len (Gauge E,m) & 1 < j & j + 1 < width (Gauge E,m) implies for i1, j1 being Element of 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) ) ; :: thesis: for i1, j1 being Element of 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:235, 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:22;
A8: 2 |^ (n -' m) > 0 by NEWTON:102;
A9: i - 3 = i -' 3 by A2, XREAL_1:235;
then i -' 3 < i -' 2 by A5, XREAL_1:12;
then (2 |^ (n -' m)) * (i -' 3) < (2 |^ (n -' m)) * (i -' 2) by A8, XREAL_1:70;
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:8;
A11: i -' 1 = i - 1 by A2, XREAL_1:235, 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:22;
then A13: (2 |^ (n -' m)) * (i -' 2) > 0 by A8, A5, XREAL_1:131;
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:237, XXREAL_0:2;
let i1, j1 be Element of NAT ; :: thesis: ( 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 ; :: thesis: cell (Gauge E,n),(i1 -' 1),j1 c= cell (Gauge E,m),(i -' 1),j
i1 < i1 + 1 by XREAL_1:31;
then A18: i1 - 1 < i1 by XREAL_1:21;
i1 > 0 + 2 by A16, A5, A13, XREAL_1:8;
then A19: i1 -' 1 < i1 by A18, XREAL_1:235, XXREAL_0:2;
j - 2 < j - 1 by XREAL_1:12;
then (2 |^ (n -' m)) * (j - 2) < (2 |^ (n -' m)) * (j - 1) by A8, XREAL_1:70;
then j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 by A17, XREAL_1:8;
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, Th68; :: thesis: verum