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 A1: ( x + y < z & not x < z - y ) ; :: thesis: contradiction
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 contradiction by A2, A1, SURREALO:4; :: thesis: verum

end;

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