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

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

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

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

end;

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

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

end;

end;