:: deftheorem Def15 defines comp SURREALR:def 15 :
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 ) ) );