theorem Th34: :: JORDAN1A:34

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