ex i being Nat st
( 0 <= i & i <= 2 |^ n & 0 / (2 |^ n) = i / (2 |^ n) ) ;
hence not dyadic n is empty by Def1; :: thesis: verum