theorem Th61: :: SURREALC:61

for x, y being Surreal st not x == 0_No & not y == 0_No holds
( omega-y x = omega-y y iff |.x.|,|.y.| are_commensurate )