let x, y, z be Real; :: 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:7;
hence ( x + y >= z & y >= z - x ) by XREAL_1:20; :: thesis: verum