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

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