let i, m, n be Nat; :: thesis: 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)) )
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( m <= n & 1 < i & i + 1 < width (Gauge (D,m)) implies ( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= width (Gauge (D,n)) ) )
( len (Gauge (D,n)) = width (Gauge (D,n)) & len (Gauge (D,m)) = width (Gauge (D,m)) ) by JORDAN8:def 1;
hence ( m <= n & 1 < i & i + 1 < width (Gauge (D,m)) implies ( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= width (Gauge (D,n)) ) ) by Th34; :: thesis: verum