:: deftheorem Def7 defines omega-y SURREALC:def 7 :
for x being Surreal st not x == 0_No holds
for b₂ being uSurreal holds
( b₂ = omega-y x iff |.x.|, No_omega^ b₂ are_commensurate );