:: deftheorem Def7 defines uReal SURREALN:def 7 :
for b₁ being ManySortedSet of REAL holds
( b₁ = uReal iff for r being Real holds b₁ . r = Unique_No (sReal . r) );