D is dense by Lm1;
hence DYADIC is dense Subset of I[01] ; :: thesis: verum