:: deftheorem defines infinitely< SURREALC:def 3 :
for x, y being Surreal holds
( x infinitely< y iff for r being positive Real holds x * (uReal . r) < y );