consider y being Surreal such that
A2: |.x.|, No_omega^ y are_commensurate by A1, Th36, Lm6;
set c = Unique_No y;
Unique_No y == y by SURREALO:def 10;
then No_omega^ (Unique_No y) == No_omega^ y by Lm5;
then No_omega^ (Unique_No y), No_omega^ y are_commensurate by Th2, Th5;
hence ex b₁ being uSurreal st |.x.|, No_omega^ b₁ are_commensurate by A2, Th4; :: thesis: verum