for n being Nat holds 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)