theorem :: SURREALR:55
for x1, x2, y1, y2 being Surreal st x1 < x2 & y1 < y2 holds
(x1 * y2) + (x2 * y1) < (x1 * y1) + (x2 * y2) by Th51;