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