:: deftheorem Def4 defines DYADIC SURREALN:def 4 :
for n being Nat
for b₂ being Subset of DYADIC holds
( b₂ = DYADIC n iff for d being Dyadic holds
( d in b₂ iff ex i being Integer st d = i / (2 |^ n) ) );