theorem Th54: :: SURREALC:54

for x, y being Surreal st x, No_omega^ y are_commensurate holds
ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x