for n being Nat
for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds
((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))