let n be Element of 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 )
A1: 0 < 2 |^ n by NEWTON:83;
( x1 = (axis x1) / (2 |^ n) & x2 = (axis x2) / (2 |^ n) ) by Th16;
hence ( x1 < x2 implies axis x1 < axis x2 ) by A1, XREAL_1:72; :: thesis: verum