let n be Nat; :: thesis: for x1, x2 being Element of dyadic n st x1 < x2 holds
( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 )
let x1, x2 be Element of dyadic n; :: thesis: ( x1 < x2 implies ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) )
assume A1: x1 < x2 ; :: thesis: ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 )
then axis x1 < axis x2 by Th14;
then A2: (axis x1) + 1 <= axis x2 by NAT_1:13;
axis x1 < axis x2 by A1, Th14;
then (axis x1) + 1 <= axis x2 by NAT_1:13;
then A3: axis x1 <= (axis x2) - 1 by XREAL_1:19;
A4: ((axis x1) + 1) / (2 |^ n) <= (axis x2) / (2 |^ n) by A2, XREAL_1:72;
(axis x1) / (2 |^ n) <= ((axis x2) - 1) / (2 |^ n) by A3, XREAL_1:72;
hence ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) by A4, Th10; :: thesis: verum