let x, y, z, t be Surreal; :: thesis: ( x <= y & z <= t implies x + z <= y + t )
assume ( x <= y & z <= t ) ; :: thesis: x + z <= y + t
then ( x + z <= y + z & y + z <= y + t ) by Th32;
hence x + z <= y + t by SURREALO:4; :: thesis: verum