:: deftheorem Def3 defines DYADIC SURREALN:def 3 :
for b₁ being set holds
( b₁ = DYADIC iff for o being object holds
( o in b₁ iff o is dyadic-like Rational ) );