theorem Th32: :: JORDAN1A:32

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