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