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