:: deftheorem Def5 defines uDyadic SURREALN:def 5 :
for b₁ being ManySortedSet of DYADIC holds
( b₁ = uDyadic iff for i, j being Integer
for p being Nat holds
( b₁ . i = uInt . i & b₁ . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(b₁ . (j / (2 |^ p)))},{(b₁ . ((j + 1) / (2 |^ p)))}] ) );