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
( x * (uReal . r) == y * (uReal . r) & y * (uReal . r) < z ) by A1, SURREALR:51;
hence x * (uReal . r) < z by SURREALO:4; :: thesis: verum