let x, y be Surreal; :: thesis: ( x,y are_commensurate implies x is positive )
assume that
A1: x,y are_commensurate and
A2: not x is positive ; :: thesis: contradiction
consider n being positive Nat such that
A3: x < (uInt . n) * y by A1;
consider m being positive Nat such that
A4: y < (uInt . m) * x by A1;
uInt . n is positive ;
then A5: y * (uInt . n) < (uInt . n) * ((uInt . m) * x) by SURREALR:70, A4;
( (uInt . n) * ((uInt . m) * x) == ((uInt . n) * (uInt . m)) * x & ((uInt . n) * (uInt . m)) * x == (uInt . (n * m)) * x ) by SURREALR:51, SURREALR:69, SURREALN:15;
then (uInt . n) * ((uInt . m) * x) == (uInt . (n * m)) * x by SURREALO:4;
then A6: y * (uInt . n) <= (uInt . (n * m)) * x by A5, SURREALO:4;
then A7: x < (uInt . (n * m)) * x by A3, SURREALO:4;

per cases ( n * m = 1 or ( x < 0_No & n * m <> 1 ) or 0_No <= x ) ;

suppose n * m = 1 ; :: thesis: contradiction

hence contradiction by A6, A3, SURREALN:11; :: thesis: verum

end;

suppose A8: ( x < 0_No & n * m <> 1 ) ; :: thesis: contradiction

1 <= n * m by NAT_1:14;
then 1 < n * m by A8, XXREAL_0:1;
then ( (uInt . (n * m)) * x < (uInt . 1) * x & (uInt . 1) * x = 1_No * x ) by A8, SURREALR:71, SURREALN:9, SURREALN:11;
then (uInt . (n * m)) * x <= x ;
hence contradiction by A6, A3, SURREALO:4; :: thesis: verum

end;

suppose A9: 0_No <= x ; :: thesis: contradiction

then x == 0_No by A2;
then ( (uInt . (n * m)) * x == (uInt . (n * m)) * 0_No & (uInt . (n * m)) * 0_No = 0_No ) by SURREALR:51;
hence contradiction by A9, A7, SURREALO:4; :: thesis: verum

end;

end;