let x, y, z be Surreal; :: thesis: ( x + y <= z iff x <= z - y )
thus ( x + y <= z implies x <= z - y ) :: thesis: ( x <= z - y implies x + y <= z )

proof

assume x + y <= z ; :: thesis: x <= z - y
then A1: (x + y) + (- y) <= z + (- y) by Th32;
y - y == 0_No by Th39;
then x + (y + (- y)) >= x + 0_No by Th32;
then (x + y) + (- y) >= x by Th37;
hence x <= z - y by A1, SURREALO:4; :: thesis: verum

end;

assume x <= z - y ; :: thesis: x + y <= z
then x + y <= (z + (- y)) + y by Th32;
then A2: x + y <= z + ((- y) + y) by Th37;
y - y == 0_No by Th39;
then ( z + ((- y) + y) <= z + 0_No & z + 0_No = z ) by Th32;
hence x + y <= z by A2, SURREALO:4; :: thesis: verum