for m, 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)) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )