theorem Th28: :: SURREALN:28

for d being Dyadic st 0 <= d & d is not Integer holds
ex n, m, p being Nat st
( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) )