theorem Th20: :: SURREALN:20

for d being Dyadic
for n being Nat holds
( d in (DYADIC (n + 1)) \ (DYADIC n) iff ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) )