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

proof

consider n being positive Nat such that
A2: x < (uInt . n) * z by A1;
y < (uInt . n) * z by A1, A2, SURREALO:4;
hence ex n being positive Nat st y < (uInt . n) * z ; :: thesis: verum

end;

consider n being positive Nat such that
A3: z < (uInt . n) * x by A1;
(uInt . n) * x == (uInt . n) * y by A1, SURREALR:51;
then z < (uInt . n) * y by A3, SURREALO:4;
hence ex n being positive Nat st z < (uInt . n) * y ; :: thesis: verum