:: deftheorem Def2 defines DYADIC URYSOHN1:def 2 :
for b₁ being Subset of REAL holds
( b₁ = DYADIC iff for a being Real holds
( a in b₁ iff ex n being Nat st a in dyadic n ) );