let a, b, c be Real; :: thesis: ( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) )
A1: c + (min (a,b)) = min ((c + a),(c + b))

proof

per cases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

suppose A2: min (a,b) = a ; :: thesis: c + (min (a,b)) = min ((c + a),(c + b))

then a <= b by XXREAL_0:def 9;
then a + c <= c + b by XREAL_1:6;
hence c + (min (a,b)) = min ((c + a),(c + b)) by A2, XXREAL_0:def 9; :: thesis: verum

end;

suppose A3: min (a,b) = b ; :: thesis: c + (min (a,b)) = min ((c + a),(c + b))

then a >= b by XXREAL_0:def 9;
then a + c >= b + c by XREAL_1:6;
hence c + (min (a,b)) = min ((c + a),(c + b)) by A3, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

c + (max (a,b)) = max ((c + a),(c + b))

proof

per cases ( max (a,b) = b or max (a,b) = a ) by XXREAL_0:16;

suppose A4: max (a,b) = b ; :: thesis: c + (max (a,b)) = max ((c + a),(c + b))

then a <= b by XXREAL_0:def 10;
then c + a <= c + b by XREAL_1:6;
hence c + (max (a,b)) = max ((c + a),(c + b)) by A4, XXREAL_0:def 10; :: thesis: verum

end;

suppose A5: max (a,b) = a ; :: thesis: c + (max (a,b)) = max ((c + a),(c + b))

then a >= b by XXREAL_0:def 10;
then a + c >= b + c by XREAL_1:6;
hence c + (max (a,b)) = max ((c + a),(c + b)) by A5, XXREAL_0:def 10; :: thesis: verum

end;

end;

end;

hence ( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) ) by A1; :: thesis: verum