let x, y, z be Surreal; :: thesis: ( x,y are_commensurate & z infinitely< x implies z infinitely< y )
assume A1: ( x,y are_commensurate & z infinitely< x ) ; :: thesis: z infinitely< y
then consider n being positive Nat such that
A2: x < y * (uInt . n) ;
let r be positive Real; :: according to SURREALC:def 3 :: thesis: z * (uReal . r) < y
z * (uReal . (r * n)) <= x by A1;
then A3: z * (uReal . (r * n)) < y * (uInt . n) by SURREALO:4, A2;
A4: 0_No < uReal . (1 / n) by SURREALI:def 8;
( uInt . n = uDyadic . n & uDyadic . n = uReal . n ) by SURREALN:46, SURREALN:def 5;
then ( (z * (uReal . (r * n))) * (uReal . (1 / n)) < (y * (uReal . n)) * (uReal . (1 / n)) & (y * (uReal . n)) * (uReal . (1 / n)) == y ) by A4, Lm2, A3, SURREALR:70;
then A5: (z * (uReal . (r * n))) * (uReal . (1 / n)) < y by SURREALO:4;
( (r * n) * (1 / n) = r * (n * (1 / n)) & r * (n * (1 / n)) = r * 1 ) by XCMPLX_1:106;
then ( (z * (uReal . (r * n))) * (uReal . (1 / n)) == z * ((uReal . (r * n)) * (uReal . (1 / n))) & z * ((uReal . (r * n)) * (uReal . (1 / n))) == z * (uReal . r) ) by SURREALR:69, SURREALR:51, SURREALN:57;
then (z * (uReal . (r * n))) * (uReal . (1 / n)) == z * (uReal . r) by SURREALO:4;
hence z * (uReal . r) < y by A5, SURREALO:4; :: thesis: verum