let n be Nat; :: thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1 < axis x2
let x1, x2 be Element of dyadic n; :: thesis: ( x1 < x2 implies axis x1 < axis x2 )
( x1 = (axis x1) / (2 |^ n) & x2 = (axis x2) / (2 |^ n) ) by Th10;
hence ( x1 < x2 implies axis x1 < axis x2 ) by XREAL_1:72; :: thesis: verum