y - z <= y - 0 by XREAL_1:10;
then max ((y - z),y) = y by XXREAL_0:def 10;
hence max ((max (x,y)),(y - z)) = max (x,y) by XXREAL_0:34; :: thesis: verum