theorem :: SURREALC:55
for x, y being Surreal
for r being Real st x is positive & |.(x - ((No_omega^ y) * (uReal . r))).| infinitely< x holds
r is positive