theorem Th35: :: JORDAN1A:35

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