let n be Element of NAT ; :: thesis: for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds
((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1))
let x1, x2 be Element of dyadic (n + 1); :: thesis: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n implies ((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1)) )
assume that
A1: x1 < x2 and
A2: not x1 in dyadic n and
A3: not x2 in dyadic n ; :: thesis: ((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1))
consider k2 being Element of NAT such that
A4: ( axis x2,(n + 1) = 2 * k2 or axis x2,(n + 1) = (2 * k2) + 1 ) by SCHEME1:1;
A5: axis x2,(n + 1) <> k2 * 2

proof

assume A6: axis x2,(n + 1) = k2 * 2 ; :: thesis: contradiction
then x2 = (k2 * 2) / (2 |^ (n + 1)) by Th16;
then A7: x2 = (k2 * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k2 / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k2 / (2 |^ n) ;
k2 * 2 <= 2 |^ (n + 1) by A6, Th16;
then k2 * 2 <= (2 |^ n) * 2 by NEWTON:11;
then A8: k2 <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
0 <= k2 by NAT_1:2;
hence contradiction by A3, A7, A8, Def3; :: thesis: verum

end;

consider k1 being Element of NAT such that
A9: ( axis x1,(n + 1) = 2 * k1 or axis x1,(n + 1) = (2 * k1) + 1 ) by SCHEME1:1;
A10: not axis x1,(n + 1) = k1 * 2

proof

assume A11: axis x1,(n + 1) = k1 * 2 ; :: thesis: contradiction
then x1 = (k1 * 2) / (2 |^ (n + 1)) by Th16;
then A12: x1 = (k1 * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k1 / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k1 / (2 |^ n) ;
k1 * 2 <= 2 |^ (n + 1) by A11, Th16;
then k1 * 2 <= (2 |^ n) * 2 by NEWTON:11;
then A13: k1 <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
0 <= k1 by NAT_1:2;
hence contradiction by A2, A12, A13, Def3; :: thesis: verum

end;

then (k1 * 2) + 1 < (k2 * 2) + 1 by A1, A9, A4, A5, Th21;
then ((k1 * 2) + 1) + (- 1) < ((k2 * 2) + 1) + (- 1) by XREAL_1:8;
then (k1 * 2) / 2 < (k2 * 2) / 2 by XREAL_1:76;
then k1 + 1 <= k2 by NAT_1:13;
then ( 0 < 2 |^ (n + 1) & (k1 + 1) * 2 <= k2 * 2 ) by NEWTON:102, XREAL_1:66;
hence ((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1)) by A9, A4, A10, A5, XREAL_1:74; :: thesis: verum