theorem Th37: :: JORDAN1H:37

for m, j, i, n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Nat st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )