theorem Th15: :: URYSOHN1:15

for n being Nat
for x1, x2 being Element of dyadic n st x1 < x2 holds
( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 )