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