let x, y be Real; :: thesis: (max (x,y)) - (min (x,y)) = |.(x - y).|

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

suppose x >= y ; :: thesis: (max (x,y)) - (min (x,y)) = |.(x - y).|

then ( min (x,y) = y & max (x,y) = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (max (x,y)) - (min (x,y)) = |.(x - y).| by ABSVALUE:def 1; :: thesis: verum

end;

suppose A1: x < y ; :: thesis: (max (x,y)) - (min (x,y)) = |.(x - y).|

then A2: ( min (x,y) = x & max (x,y) = y ) by XXREAL_0:def 9, XXREAL_0:def 10;
x - y < x - x by A1, XREAL_1:10;
then |.(x - y).| = - (x - y) by ABSVALUE:def 1;
hence (max (x,y)) - (min (x,y)) = |.(x - y).| by A2; :: thesis: verum

end;

end;