let y1, y2 be uSurreal; :: thesis: ( |.x.|, No_omega^ y1 are_commensurate & |.x.|, No_omega^ y2 are_commensurate implies y1 = y2 )
assume that
A3: |.x.|, No_omega^ y1 are_commensurate and
A4: |.x.|, No_omega^ y2 are_commensurate ; :: thesis: y1 = y2
y1 == y2 by A1, Th36, A3, A4, Lm7;
hence y1 = y2 by SURREALO:50; :: thesis: verum