let r be positive Real; :: thesis: for x, y being Surreal st x infinitely< y holds
( x * (uReal . r) infinitely< y & x infinitely< y * (uReal . r) )
let x, y be Surreal; :: thesis: ( x infinitely< y implies ( x * (uReal . r) infinitely< y & x infinitely< y * (uReal . r) ) )
assume A1: x infinitely< y ; :: thesis: ( x * (uReal . r) infinitely< y & x infinitely< y * (uReal . r) )
thus x * (uReal . r) infinitely< y :: thesis: x infinitely< y * (uReal . r)

proof

let s be positive Real; :: according to SURREALC:def 3 :: thesis: (x * (uReal . r)) * (uReal . s) < y
( (x * (uReal . r)) * (uReal . s) == x * ((uReal . s) * (uReal . r)) & x * ((uReal . s) * (uReal . r)) == x * (uReal . (s * r)) ) by SURREALN:57, SURREALR:69, SURREALR:51;
then ( (x * (uReal . r)) * (uReal . s) == x * (uReal . (s * r)) & x * (uReal . (s * r)) < y ) by A1, SURREALO:4;
hence (x * (uReal . r)) * (uReal . s) < y by SURREALO:4; :: thesis: verum

end;

let s be positive Real; :: according to SURREALC:def 3 :: thesis: x * (uReal . s) < y * (uReal . r)
A2: 0_No < uReal . r by SURREALI:def 8;
A3: (x * (uReal . (s * (1 / r)))) * (uReal . r) < y * (uReal . r) by A1, A2, SURREALR:70;
s * ((1 / r) * r) = s * 1 by XCMPLX_1:106;
then (s * (1 / r)) * r = s ;
then ( (x * (uReal . (s * (1 / r)))) * (uReal . r) == x * ((uReal . (s * (1 / r))) * (uReal . r)) & x * ((uReal . (s * (1 / r))) * (uReal . r)) == x * (uReal . s) ) by SURREALR:69, SURREALR:51, SURREALN:57;
then (x * (uReal . (s * (1 / r)))) * (uReal . r) == x * (uReal . s) by SURREALO:4;
hence x * (uReal . s) < y * (uReal . r) by A3, SURREALO:4; :: thesis: verum