for n being Nat
for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1 < axis x2