:: deftheorem Def14 defines comp SURREALR:def 14 :
for x, y being Surreal
for X, Y, b₅ being set holds
( b₅ = comp (X,x,y,Y) iff for o being object holds
( o in b₅ iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) ) );