:: deftheorem Def1 defines dyadic URYSOHN1:def 1 :
for n being Nat
for b₂ being Subset of REAL holds
( b₂ = dyadic n iff for x being Real holds
( x in b₂ iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) );