theorem :: SURREALC:60

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))