let n be Element of NAT ; :: thesis: 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
( (2 * 0 ) + 1 = 1 & 0 < 2 |^ n ) by NEWTON:102;
hence 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by Th14; :: thesis: verum