theorem Th20: :: SURREALC:20

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