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

per cases ( a >= b or a < b ) ;

suppose a >= b ; :: thesis: a + b = (min (a,b)) + (max (a,b))

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

end;

suppose a < b ; :: thesis: a + b = (min (a,b)) + (max (a,b))

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

end;

end;