let n be Element of NAT ; :: thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
axis x1,n < axis x2,n
let x1, x2 be Element of dyadic n; :: thesis: ( x1 < x2 implies axis x1,n < axis x2,n )
A1: ( x1 = (axis x1,n) / (2 |^ n) & x2 = (axis x2,n) / (2 |^ n) ) by Th16;
0 < 2 |^ n by NEWTON:102;
hence ( x1 < x2 implies axis x1,n < axis x2,n ) by A1, XREAL_1:74; :: thesis: verum