theorem Th47: :: JORDAN1A:47

for i, j, m, n being 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)