let x, y be Real; :: thesis: (min (x,y)) + (max (x,y)) = x + y

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

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

then min (x,y) = x by XXREAL_0:def 9;
hence (min (x,y)) + (max (x,y)) = x + y by A1, XXREAL_0:def 10; :: thesis: verum

end;

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

then min (x,y) = y by XXREAL_0:def 9;
hence (min (x,y)) + (max (x,y)) = x + y by A2, XXREAL_0:def 10; :: thesis: verum

end;

end;