let x, y, z be Surreal; :: thesis: ( x,y are_commensurate & y,z are_commensurate implies x,z are_commensurate )
assume A1: ( x,y are_commensurate & y,z are_commensurate ) ; :: thesis: x,z are_commensurate
thus ex n being positive Nat st x < (uInt . n) * z :: according to SURREALC:def 2 :: thesis: ex n being positive Nat st z < (uInt . n) * x

proof

consider n being positive Nat such that
A2: x < (uInt . n) * y by A1;
consider m being positive Nat such that
A3: y < (uInt . m) * z by A1;
take nm = n * m; :: thesis: x < (uInt . nm) * z
uInt . n is positive ;
then A4: (uInt . n) * y < (uInt . n) * ((uInt . m) * z) by A3, SURREALR:70;
( (uInt . n) * ((uInt . m) * z) == ((uInt . n) * (uInt . m)) * z & ((uInt . n) * (uInt . m)) * z == (uInt . nm) * z ) by SURREALR:51, SURREALR:69, SURREALN:15;
then (uInt . n) * ((uInt . m) * z) == (uInt . nm) * z by SURREALO:4;
then (uInt . n) * y <= (uInt . nm) * z by A4, SURREALO:4;
hence x < (uInt . nm) * z by A2, SURREALO:4; :: thesis: verum

end;

consider n being positive Nat such that
A5: y < (uInt . n) * x by A1;
consider m being positive Nat such that
A6: z < (uInt . m) * y by A1;
take nm = n * m; :: thesis: z < (uInt . nm) * x
uInt . m is positive ;
then A7: (uInt . m) * y < (uInt . m) * ((uInt . n) * x) by A5, SURREALR:70;
( (uInt . m) * ((uInt . n) * x) == ((uInt . m) * (uInt . n)) * x & ((uInt . m) * (uInt . n)) * x == (uInt . nm) * x ) by SURREALR:51, SURREALR:69, SURREALN:15;
then (uInt . m) * ((uInt . n) * x) == (uInt . nm) * x by SURREALO:4;
then (uInt . m) * y <= (uInt . nm) * x by A7, SURREALO:4;
hence z < (uInt . nm) * x by A6, SURREALO:4; :: thesis: verum