:: deftheorem defines * SURREALR:def 13 :
for x, y being Surreal holds x * y = (No_mult_op ((born x) (+) (born y))) . [x,y];