let x, y, z be real number ; :: thesis: ( x >= 0 & y >= z implies ( x + y >= z & y >= z - x ) )
assume ( x >= 0 & y >= z ) ; :: thesis: ( x + y >= z & y >= z - x )
then x + y >= z + 0 by XREAL_1:9;
hence ( x + y >= z & y >= z - x ) by XREAL_1:22; :: thesis: verum