theorem Th7: :: SURREALC:7

for x, y being Surreal holds
( x,y are_commensurate iff ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) )