let x, y, z be Integer; :: thesis: max ((x + y),(x + z)) = x + (max (y,z))

per cases ( y <= z or y > z ) ;

suppose A1: y <= z ; :: thesis: max ((x + y),(x + z)) = x + (max (y,z))

then x + y <= x + z by XREAL_1:6;
hence max ((x + y),(x + z)) = x + z by XXREAL_0:def 10
.= x + (max (y,z)) by A1, XXREAL_0:def 10 ;
:: thesis: verum

end;

suppose A2: y > z ; :: thesis: max ((x + y),(x + z)) = x + (max (y,z))

then x + y > x + z by XREAL_1:8;
hence max ((x + y),(x + z)) = x + y by XXREAL_0:def 10
.= x + (max (y,z)) by A2, XXREAL_0:def 10 ;
:: thesis: verum

end;

end;