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

per cases ( x <= y or not 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: not 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;