theorem Th13: :: SURREALC:13
for r being positive Real
for x, y being Surreal st x infinitely< y holds
( x * (uReal . r) infinitely< y & x infinitely< y * (uReal . r) )