let n be Nat; :: thesis: for x being Element of dyadic n holds
( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )
let x be Element of dyadic n; :: thesis: ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )
A1: ( 0 + (axis x) < 1 + (axis x) & 0 < 2 |^ n ) by NEWTON:83, XREAL_1:8;
( x = (axis x) / (2 |^ n) & (- 1) + (axis x) < 0 + (axis x) ) by Def5, XREAL_1:8;
hence ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) by A1, XREAL_1:74; :: thesis: verum