theorem :: URYSOHN2:23

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