let x, y, z be Surreal; :: thesis: ( x,z are_commensurate & x <= y & y <= z implies ( x,y are_commensurate & y,z are_commensurate ) )
assume A1: ( x,z are_commensurate & x <= y & y <= z ) ; :: thesis: ( x,y are_commensurate & y,z are_commensurate )
A2: ( x is positive & z is positive ) by A1, Th3;

per cases ( x == y or y == z or ( x < y & y < z ) ) by A1;

suppose ( x == y or y == z ) ; :: thesis: ( x,y are_commensurate & y,z are_commensurate )

hence ( x,y are_commensurate & y,z are_commensurate ) by A1, Th5, A2, Th2; :: thesis: verum

end;

suppose A3: ( x < y & y < z ) ; :: thesis: ( x,y are_commensurate & y,z are_commensurate )

consider n being positive Nat such that
A4: z < (uInt . n) * x by A1;
y <= z by A3;
then A5: y < (uInt . n) * x by A4, SURREALO:4;
0_No < uInt . n by SURREALI:def 8;
then (uInt . n) * x <= (uInt . n) * y by A3, SURREALR:70;
then A6: z < (uInt . n) * y by A4, SURREALO:4;
A7: y < (uInt . 1) * z by A3, SURREALN:11;
y = (uInt . 1) * y by SURREALN:11;
hence ( x,y are_commensurate & y,z are_commensurate ) by A3, A7, A6, A5; :: thesis: verum

end;

end;