:: deftheorem Def6 defines sReal SURREALN:def 6 :
for b₁ being ManySortedSet of REAL holds
( b₁ = sReal iff for r being Real holds b₁ . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] );