let n be Nat; :: thesis: 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
( (2 * 0) + 1 = 1 & 0 < 2 |^ n ) by NEWTON:83;
hence 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by Th8; :: thesis: verum