let n be Element of NAT ; :: thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
( x1 <= ((axis x2,n) - 1) / (2 |^ n) & ((axis x1,n) + 1) / (2 |^ n) <= x2 )
let x1, x2 be Element of dyadic n; :: thesis: ( x1 < x2 implies ( x1 <= ((axis x2,n) - 1) / (2 |^ n) & ((axis x1,n) + 1) / (2 |^ n) <= x2 ) )
assume A1: x1 < x2 ; :: thesis: ( x1 <= ((axis x2,n) - 1) / (2 |^ n) & ((axis x1,n) + 1) / (2 |^ n) <= x2 )
then axis x1,n < axis x2,n by Th21;
then (axis x1,n) + 1 <= axis x2,n by NAT_1:13;
then A2: axis x1,n <= (axis x2,n) - 1 by XREAL_1:21;
0 < 2 |^ n by NEWTON:102;
then A3: (axis x1,n) / (2 |^ n) <= ((axis x2,n) - 1) / (2 |^ n) by A2, XREAL_1:74;
axis x1,n < axis x2,n by A1, Th21;
then A4: (axis x1,n) + 1 <= axis x2,n by NAT_1:13;
0 < 2 |^ n by NEWTON:102;
then ((axis x1,n) + 1) / (2 |^ n) <= (axis x2,n) / (2 |^ n) by A4, XREAL_1:74;
hence ( x1 <= ((axis x2,n) - 1) / (2 |^ n) & ((axis x1,n) + 1) / (2 |^ n) <= x2 ) by A3, Th16; :: thesis: verum