theorem Th43: :: SURREALN:43

for x being Surreal
for r being Real holds
( x in R_ (sReal . r) iff ex n being Nat st x = uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )