for n being Nat holds dyadic n c= DYADIC by URYSOHN1:def 2;