for n being Nat
for x being Element of dyadic n holds
( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) )