:: deftheorem Def1 defines *' SURREALI:def 1 :
for x, y being object st x is surreal & y is surreal holds
for b₃ being Surreal holds
( b₃ = x *' y iff for x1, y1 being Surreal st x1 = x & y1 = y holds
b₃ = x1 * y1 );