let x, y be Surreal; :: thesis: for r, r1, r2 being Real st x * (uReal . r1) < y * (uReal . r2) & 0 < r holds
x * (uReal . (r1 * r)) < y * (uReal . (r2 * r))
let r, r1, r2 be Real; :: thesis: ( x * (uReal . r1) < y * (uReal . r2) & 0 < r implies x * (uReal . (r1 * r)) < y * (uReal . (r2 * r)) )
assume A1: ( x * (uReal . r1) < y * (uReal . r2) & 0 < r ) ; :: thesis: x * (uReal . (r1 * r)) < y * (uReal . (r2 * r))
then 0_No < uReal . r by SURREALI:def 8;
then A2: (x * (uReal . r1)) * (uReal . r) < (y * (uReal . r2)) * (uReal . r) by A1, SURREALR:70;
(x * (uReal . r1)) * (uReal . r) == x * (uReal . (r1 * r)) by Lm1;
then ( x * (uReal . (r1 * r)) < (y * (uReal . r2)) * (uReal . r) & (y * (uReal . r2)) * (uReal . r) == y * (uReal . (r2 * r)) ) by A2, SURREALO:4, Lm1;
hence x * (uReal . (r1 * r)) < y * (uReal . (r2 * r)) by SURREALO:4; :: thesis: verum