theorem Th42: :: SURREALN:42

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