set x = 0 / (2 |^ n);
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & 0 / (2 |^ n) = i / (2 |^ n) )

proof

take 0 ; :: thesis: ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) )
thus ( 0 <= 0 & 0 <= 2 |^ n & 0 / (2 |^ n) = 0 / (2 |^ n) ) by NEWTON:83; :: thesis: verum

end;

hence not dyadic n is empty by Def3; :: thesis: verum