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