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

( 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