theorem Th12: :: URYSOHN1:12

for n being Nat
for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n)