per cases ( a = b or a > b or a < b ) by XXREAL_0:1;

suppose a = b ; :: thesis: (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b

hence (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b ; :: thesis: verum

end;

suppose B1: a > b ; :: thesis: (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b

then B2: ( max (a,b) = a & min (a,b) = b ) by XXREAL_0:def 9, XXREAL_0:def 10;
a - b > b - b by B1, XREAL_1:9;
then sgn (a - b) = 1 by ABSVALUE:def 2;
hence (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b by B2; :: thesis: verum

end;

suppose B1: a < b ; :: thesis: (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b

then B2: ( max (a,b) = b & min (a,b) = a ) by XXREAL_0:def 9, XXREAL_0:def 10;
a - b < b - b by B1, XREAL_1:9;
then sgn (a - b) = - 1 by ABSVALUE:def 2;
hence (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b by B2; :: thesis: verum

end;

end;