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