let x be Surreal; :: thesis: for r being Real holds
( x in L_ (sReal . r) iff ex n being Nat st x = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) )
let r be Real; :: thesis: ( x in L_ (sReal . r) iff ex n being Nat st x = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) )
sReal . r = [ { (uDyadic . ([/((r * (2 |^ k)) - 1)\] / (2 |^ k))) where k is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] by Def6;
hence ( x in L_ (sReal . r) iff ex n being Nat st x = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) ) ; :: thesis: verum