y + z >= y + 0 by XREAL_1:6;
then min (y,(y + z)) = y by XXREAL_0:def 9;
hence min ((min (x,y)),(y + z)) = min (x,y) by XXREAL_0:33; :: thesis: verum