theorem Th53: :: SURREALC:53

for x, y being Surreal
for r being Real st 0_No <= x & x infinitely< y holds
|.(x * (uReal . r)).| infinitely< y