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 SURREALN:51, SURREALN:47;
then A2: (x * (uReal . r1)) * (uReal . r) <= (y * (uReal . r2)) * (uReal . r) by A1, SURREALR:75;
(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