let x, y, z be Surreal; :: thesis: ( x infinitely< y & y infinitely< z implies x infinitely< z )
assume A1: ( x infinitely< y & y infinitely< z ) ; :: thesis: x infinitely< z
let r be positive Real; :: according to SURREALC:def 3 :: thesis: x * (uReal . r) < z
y * (uReal . 1) < z by A1;
then y <= z by SURREALN:48;
hence x * (uReal . r) < z by A1, SURREALO:4; :: thesis: verum