let n be Element of NAT ; :: thesis: for x being Element of dyadic n holds ((axis x,n) - 1) / (2 |^ n) < ((axis x,n) + 1) / (2 |^ n)
let x be Element of dyadic n; :: thesis: ((axis x,n) - 1) / (2 |^ n) < ((axis x,n) + 1) / (2 |^ n)
( (- 1) + (axis x,n) < 1 + (axis x,n) & 0 < 2 |^ n ) by NEWTON:102, XREAL_1:10;
hence ((axis x,n) - 1) / (2 |^ n) < ((axis x,n) + 1) / (2 |^ n) by XREAL_1:76; :: thesis: verum