for n being Nat holds
( 0 in dyadic n & 1 in dyadic n )