theorem Th31: :: JORDAN14:31

for C being Subset of (TOP-REAL 2)
for n, m, i being Nat st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds
(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))