let x, y be Surreal; :: thesis: for x1, x1R, y1, y1R being Surreal st 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 holds
x * x1R < y * y1R
let x1, x1R, y1, y1R be Surreal; :: thesis: ( 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 implies x * x1R < y * y1R )
assume A1: ( 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 ) ; :: thesis: x * x1R < y * y1R
A2: ( 0_No <= x1 & 0_No <= y1 ) by A1;
1_No is positive ;
then ( 0_No < x1 * x1R & 0_No < y1 * y1R ) by A1, SURREALO:4;
then A3: ( 0_No < x1R & 0_No < y1R ) by A2, SURREALR:72;
then (x * y1) * y1R < (y * x1) * y1R by A1, SURREALR:70;
then A4: ((x * y1) * y1R) * x1R < ((y * x1) * y1R) * x1R by A3, SURREALR:70;
( (x * y1) * y1R == x * (y1 * y1R) & x * (y1 * y1R) == x * 1_No & x * 1_No = x ) by SURREALR:51, SURREALR:69, A1;
then (x * y1) * y1R == x by SURREALO:4;
then A5: ((x * y1) * y1R) * x1R == x * x1R by SURREALR:51;
( ((y * x1) * y1R) * x1R == (y * (x1 * y1R)) * x1R & (y * (x1 * y1R)) * x1R == y * ((x1 * y1R) * x1R) ) by SURREALR:51, SURREALR:69;
then ( ((y * x1) * y1R) * x1R == y * ((x1 * y1R) * x1R) & y * ((x1 * y1R) * x1R) == y * (y1R * (x1 * x1R)) ) by SURREALR:69, SURREALO:4, SURREALR:51;
then A6: ((y * x1) * y1R) * x1R == y * (y1R * (x1 * x1R)) by SURREALO:4;
( y1R * (x1 * x1R) == y1R * 1_No & y1R * 1_No = y1R ) by SURREALR:51, A1;
then y * (y1R * (x1 * x1R)) == y * y1R by SURREALR:51;
then ((y * x1) * y1R) * x1R == y * y1R by A6, SURREALO:4;
then ((x * y1) * y1R) * x1R < y * y1R by A4, SURREALO:4;
hence x * x1R < y * y1R by A5, SURREALO:4; :: thesis: verum