let x be Surreal; :: thesis: ( x is positive implies x,x are_commensurate )
assume x is positive ; :: thesis: x,x are_commensurate
then A1: ( x = 0_No + x & 0_No + x < x + x ) by SURREALR:44;
A2: 1_No + 1_No = uInt . (1 + 1) by SURREALN:11, SURREALN:13;
1_No * x = x ;
then x + x == (1_No + 1_No) * x by SURREALR:67;
then x < (uInt . (1 + 1)) * x by A2, A1, SURREALO:4;
hence x,x are_commensurate ; :: thesis: verum