D is dense

proof

thus Cl D = [#] I[01] by Lm1; :: according to TOPS_1:def 3 :: thesis: verum

end;

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