let x, y be Surreal; :: thesis: ( x,y are_commensurate iff ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) )
thus ( x,y are_commensurate implies ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) ) :: thesis: ( ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) implies x,y are_commensurate )

proof

assume A1: x,y are_commensurate ; :: thesis: ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x )
A2: ( x is positive & y is positive ) by A1, Th3;
consider n being positive Nat such that
A3: x < (uInt . n) * y by A1;
consider m being positive Nat such that
A4: y < (uInt . m) * x by A1;
take n + m ; :: thesis: ( x < (uInt . (n + m)) * y & y < (uInt . (n + m)) * x )
( n + 0 < n + m & m + 0 < n + m ) by XREAL_1:6;
then ( (uInt . n) * y <= (uInt . (n + m)) * y & (uInt . m) * x <= (uInt . (n + m)) * x ) by A2, SURREALR:70, SURREALN:9;
hence ( x < (uInt . (n + m)) * y & y < (uInt . (n + m)) * x ) by A3, A4, SURREALO:4; :: thesis: verum

end;

thus ( ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) implies x,y are_commensurate ) ; :: thesis: verum