theorem Th51: :: SURREALR:51

( ( for x, y being Surreal holds x * y is Surreal ) & ( for x, y being Surreal holds x * y = y * x ) & ( for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y ) & ( for x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 being Surreal st x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 holds
x1y2 + x2y1 < x1y1 + x2y2 ) )