let a, b, c be Element of REAL ; :: thesis: ( c + (max a,b) = max (c + a),(c + b) & c + (min a,b) = min (c + a),(c + b) )
A1: 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 A2: max a,b = b ; :: thesis: c + (max a,b) = max (c + a),(c + b)

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

proof

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

end;

hence c + (max a,b) = max (c + a),(c + b) ; :: thesis: verum

end;

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

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

proof

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

end;

hence c + (max a,b) = max (c + a),(c + b) ; :: thesis: verum

end;

end;

end;

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 A4: min a,b = a ; :: thesis: c + (min a,b) = min (c + a),(c + b)

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

proof

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

end;

hence c + (min a,b) = min (c + a),(c + b) ; :: thesis: verum

end;

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

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

proof

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

end;

hence c + (min a,b) = min (c + a),(c + b) ; :: 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