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

per cases ( r is positive or r <= 0 ) ;

suppose r is positive ; :: thesis: x * (uReal . r) < y

hence x * (uReal . r) < y by A1; :: thesis: verum

end;

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

then uReal . r <= 0_No by SURREALN:51, SURREALN:47;
then (uReal . r) * x <= 0_No * x by A1, SURREALR:75;
then ( (uReal . r) * x <= x & x < y ) by A1, SURREALO:4, Th9;
hence x * (uReal . r) < y by SURREALO:4; :: thesis: verum

end;

end;