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 & 1 < i & i + 1 < len (Gauge E,m) & 1 < j & j + 1 < width (Gauge E,m) holds
for i1, j1 being Element of 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); :: thesis: ( m <= n & 1 < i & i + 1 < len (Gauge E,m) & 1 < j & j + 1 < width (Gauge E,m) implies for i1, j1 being Element of 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) ; :: thesis: for i1, j1 being Element of 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
i < i + 1 by XREAL_1:31;
then A6: i < len (Gauge E,m) by A3, XXREAL_0:2;
j < j + 1 by XREAL_1:31;
then A7: j < width (Gauge E,m) by A5, XXREAL_0:2;
A8: 1 + 1 <= i by A2, NAT_1:13;
A9: 1 + 1 <= j by A4, NAT_1:13;
let i1, j1 be Element of NAT ; :: thesis: ( ((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
A10: ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 and
A11: i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 and
A12: ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 and
A13: j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 ; :: thesis: cell (Gauge E,n),i1,j1 c= cell (Gauge E,m),i,j
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in cell (Gauge E,n),i1,j1 or e in cell (Gauge E,m),i,j )
assume A14: e in cell (Gauge E,n),i1,j1 ; :: thesis: e in cell (Gauge E,m),i,j
then reconsider p = e as Point of (TOP-REAL 2) ;
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;
((2 |^ (n -' m)) * (i - 1)) + 2 <= len (Gauge E,n) by A1, A2, A3, Th55;
then A15: i1 < len (Gauge E,n) by A11, XXREAL_0:2;
then A16: i1 + 1 <= len (Gauge E,n) by NAT_1:13;
((2 |^ (n -' m)) * (j - 1)) + 2 <= width (Gauge E,n) by A1, A4, A5, Th56;
then A17: j1 < width (Gauge E,n) by A13, XXREAL_0:2;
then A18: j1 + 1 <= width (Gauge E,n) by NAT_1:13;
A19: 1 <= ((2 |^ (n -' m)) * (i - 2)) + 2 by A1, A2, A6, Th52;
then A20: 1 <= i1 by A10, XXREAL_0:2;
A21: 1 <= ((2 |^ (n -' m)) * (j - 2)) + 2 by A1, A4, A7, Th53;
then A22: 1 <= j1 by A12, XXREAL_0:2;
then A23: ( ((Gauge E,n) * i1,j1) `1 <= p `1 & p `1 <= ((Gauge E,n) * (i1 + 1),j1) `1 & ((Gauge E,n) * i1,j1) `2 <= p `2 & p `2 <= ((Gauge E,n) * i1,(j1 + 1)) `2 ) by A14, A16, A18, A20, JORDAN9:19;
A24: ( ((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (j -' 2)) + 2 = ((2 |^ (n -' m)) * (j - 2)) + 2 ) by A8, A9, XREAL_1:235;
then A25: (Gauge E,m) * i,j = (Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2) by A1, A2, A4, A6, A7, Th54;
A26: ((2 |^ (n -' m)) * (i -' 2)) + 2 <= len (Gauge E,n) by A10, A15, A24, XXREAL_0:2;
A27: ((2 |^ (n -' m)) * (j -' 2)) + 2 <= width (Gauge E,n) by A12, A17, A24, XXREAL_0:2;
( ((2 |^ (n -' m)) * (i -' 2)) + 2 < i1 or ((2 |^ (n -' m)) * (i -' 2)) + 2 = i1 ) by A10, A24, XXREAL_0:1;
then A28: ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),j1) `1 <= ((Gauge E,n) * i1,j1) `1 by A15, A17, A19, A22, A24, GOBOARD5:4;
((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),j1) `1 = ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),1) `1 by A17, A19, A22, A24, A26, GOBOARD5:3
.= ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2)) `1 by A19, A21, A24, A26, A27, GOBOARD5:3 ;
then A29: ((Gauge E,m) * i,j) `1 <= p `1 by A23, A25, A28, XXREAL_0:2;
A30: 1 < i + 1 by A2, XREAL_1:31;
A31: 1 < j + 1 by A4, XREAL_1:31;
A32: 1 < i1 + 1 by A20, NAT_1:13;
A33: 1 < j1 + 1 by A22, NAT_1:13;
A34: (i + 1) - (1 + 1) = i - 1
.= i -' 1 by A2, XREAL_1:235 ;
A35: (j + 1) - (1 + 1) = j - 1
.= j -' 1 by A4, XREAL_1:235 ;
A36: ( ((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (j -' 2)) + 2 = ((2 |^ (n -' m)) * (j - 2)) + 2 ) by A8, A9, XREAL_1:235;
then A37: (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, A7, A30, A34, Th54;
A38: i - 1 = i -' 1 by A2, XREAL_1:235;
then A39: ((2 |^ (n -' m)) * (i -' 1)) + 2 <= len (Gauge E,n) by A1, A2, A3, Th55;
i1 + 1 <= ((2 |^ (n -' m)) * (i -' 1)) + 2 by A11, A38, NAT_1:13;
then ( i1 + 1 < ((2 |^ (n -' m)) * (i -' 1)) + 2 or i1 + 1 = ((2 |^ (n -' m)) * (i -' 1)) + 2 ) by XXREAL_0:1;
then A40: ((Gauge E,n) * (i1 + 1),j1) `1 <= ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 1)) + 2),j1) `1 by A17, A22, A32, A39, GOBOARD5:4;
A41: 1 < ((2 |^ (n -' m)) * (i -' 1)) + 2 by A11, A20, A38, 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 A17, A22, A39, GOBOARD5:3
.= ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 1)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2)) `1 by A21, A27, A36, A39, A41, GOBOARD5:3 ;
then A42: p `1 <= ((Gauge E,m) * (i + 1),j) `1 by A23, A37, A40, XXREAL_0:2;
( ((2 |^ (n -' m)) * (j -' 2)) + 2 < j1 or ((2 |^ (n -' m)) * (j -' 2)) + 2 = j1 ) by A12, A36, XXREAL_0:1;
then A43: ((Gauge E,n) * i1,(((2 |^ (n -' m)) * (j -' 2)) + 2)) `2 <= ((Gauge E,n) * i1,j1) `2 by A15, A17, A20, A21, A36, GOBOARD5:5;
((Gauge E,n) * i1,(((2 |^ (n -' m)) * (j -' 2)) + 2)) `2 = ((Gauge E,n) * 1,(((2 |^ (n -' m)) * (j -' 2)) + 2)) `2 by A15, A20, A21, A27, A36, GOBOARD5:2
.= ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 2)) + 2)) `2 by A19, A21, A26, A27, A36, GOBOARD5:2 ;
then A44: ((Gauge E,m) * i,j) `2 <= p `2 by A23, A25, A43, XXREAL_0:2;
A45: ( ((2 |^ (n -' m)) * (i -' 2)) + 2 = ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (j -' 2)) + 2 = ((2 |^ (n -' m)) * (j - 2)) + 2 ) by A8, A9, XREAL_1:235;
then A46: (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, A6, A31, A35, Th54;
A47: j - 1 = j -' 1 by A4, XREAL_1:235;
then A48: ((2 |^ (n -' m)) * (j -' 1)) + 2 <= width (Gauge E,n) by A1, A4, A5, Th56;
j1 + 1 <= ((2 |^ (n -' m)) * (j -' 1)) + 2 by A13, A47, NAT_1:13;
then ( j1 + 1 < ((2 |^ (n -' m)) * (j -' 1)) + 2 or j1 + 1 = ((2 |^ (n -' m)) * (j -' 1)) + 2 ) by XXREAL_0:1;
then A49: ((Gauge E,n) * i1,(j1 + 1)) `2 <= ((Gauge E,n) * i1,(((2 |^ (n -' m)) * (j -' 1)) + 2)) `2 by A15, A20, A33, A48, GOBOARD5:5;
A50: 1 < ((2 |^ (n -' m)) * (j -' 1)) + 2 by A13, A22, A47, 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 A15, A20, A48, GOBOARD5:2
.= ((Gauge E,n) * (((2 |^ (n -' m)) * (i -' 2)) + 2),(((2 |^ (n -' m)) * (j -' 1)) + 2)) `2 by A19, A26, A45, A48, A50, GOBOARD5:2 ;
then p `2 <= ((Gauge E,m) * i,(j + 1)) `2 by A23, A46, A49, XXREAL_0:2;
hence e in cell (Gauge E,m),i,j by A2, A3, A4, A5, A29, A42, A44, JORDAN9:19; :: thesis: verum