:: deftheorem Def8 defines omega-r SURREALC:def 8 :
for x being Surreal st not x == 0_No holds
for b₂ being non zero Real holds
( b₂ = omega-r x iff |.(x - ((No_omega^ (omega-y x)) * (uReal . b₂))).| infinitely< |.x.| );