theorem Th31: :: JORDAN1A:31

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