let x, y be Surreal; :: thesis: for r being Real st 0_No <= x & x infinitely< y holds
|.(x * (uReal . r)).| infinitely< y
let r be Real; :: thesis: ( 0_No <= x & x infinitely< y implies |.(x * (uReal . r)).| infinitely< y )
assume A1: ( 0_No <= x & x infinitely< y ) ; :: thesis: |.(x * (uReal . r)).| infinitely< y
let s be positive Real; :: according to SURREALC:def 3 :: thesis: |.(x * (uReal . r)).| * (uReal . s) < y

per cases ( 0_No <= x * (uReal . r) or x * (uReal . r) < 0_No ) ;

suppose 0_No <= x * (uReal . r) ; :: thesis: |.(x * (uReal . r)).| * (uReal . s) < y

then |.(x * (uReal . r)).| = x * (uReal . r) by Def6;
then ( |.(x * (uReal . r)).| * (uReal . s) == x * (uReal . (r * s)) & x * (uReal . (r * s)) < y ) by Th20, A1, Lm1;
hence |.(x * (uReal . r)).| * (uReal . s) < y by SURREALO:4; :: thesis: verum

end;

suppose x * (uReal . r) < 0_No ; :: thesis: |.(x * (uReal . r)).| * (uReal . s) < y

then A2: |.(x * (uReal . r)).| = - (x * (uReal . r)) by Def6;
x * (- (uReal . r)) == x * (uReal . (- r)) by SURREALN:56, SURREALR:51;
then - (x * (uReal . r)) == x * (uReal . (- r)) by SURREALR:58;
then ( |.(x * (uReal . r)).| * (uReal . s) == (x * (uReal . (- r))) * (uReal . s) & (x * (uReal . (- r))) * (uReal . s) == x * (uReal . ((- r) * s)) ) by A2, SURREALR:51, Lm1;
then ( |.(x * (uReal . r)).| * (uReal . s) == x * (uReal . ((- r) * s)) & x * (uReal . ((- r) * s)) < y ) by Th20, A1, SURREALO:4;
hence |.(x * (uReal . r)).| * (uReal . s) < y by SURREALO:4; :: thesis: verum

end;

end;