theorem Th73: :: SURREALC:73

for x, y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y )