theorem Th23: :: SURREALN:23

for d being Dyadic holds
( d is Integer or ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) )