:: deftheorem defines are_commensurate SURREALC:def 2 :
for x, y being Surreal holds
( x,y are_commensurate iff ( ex n being positive Nat st x < (uInt . n) * y & ex n being positive Nat st y < (uInt . n) * x ) );