let x, y, z be Real; :: thesis: ( ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) implies ( x + y > z & y > z - x ) )
assume ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) ; :: thesis: ( x + y > z & y > z - x )
then x + y > z + 0 by XREAL_1:8;
hence ( x + y > z & y > z - x ) by XREAL_1:19; :: thesis: verum