let m, n, i be Element of 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 Th55; :: thesis: verum