let x, y, z, t be Surreal; :: thesis: ( x <= y & z < t implies x + z < y + t )
assume A1: ( x <= y & z < t ) ; :: thesis: x + z < y + t
assume not x + z < y + t ; :: thesis: contradiction
then A2: z >= (y + t) - x by Th42;
A3: x - x == 0_No by Th39;
x + (- x) <= y + (- x) by A1, Th32;
then 0_No <= y + (- x) by A3, SURREALO:4;
then A4: t + 0_No <= t + (y + (- x)) by Th32;
(y + t) + (- x) = t + (y + (- x)) by Th37;
hence contradiction by A1, A2, A4, SURREALO:4; :: thesis: verum