:: deftheorem Def1 defines uInt SURREALN:def 1 :
for b₁ being ManySortedSet of INT holds
( b₁ = uInt iff for n being Nat holds
( b₁ . 0 = 0_No & b₁ . (n + 1) = [{(b₁ . n)},{}] & b₁ . (- (n + 1)) = [{},{(b₁ . (- n))}] ) );