theorem Th59: :: SURREALC:59

for x, y being Surreal
for r, r1, r2 being Real st x * (uReal . r1) < y * (uReal . r2) & 0 < r holds
x * (uReal . (r1 * r)) < y * (uReal . (r2 * r))