:: deftheorem Def8 defines ++ SURREALR:def 8 :
for X, Y, b₃ being set holds
( b₃ = X ++ Y iff for o being object holds
( o in b₃ iff ex x, y being Surreal st
( x in X & y in Y & o = x + y ) ) );