let a, b be non negative Real; :: thesis: (max (a,b)) - (min (a,b)) = |.(a - b).|

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

suppose a >= b ; :: thesis: (max (a,b)) - (min (a,b)) = |.(a - b).|

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

end;

suppose a < b ; :: thesis: (max (a,b)) - (min (a,b)) = |.(a - b).|

then ( max (a,b) = b & min (a,b) = a ) by XXREAL_0:def 9, XXREAL_0:def 10;
then |.((max (a,b)) - (min (a,b))).| = |.(- (b - a)).| by COMPLEX1:52;
hence (max (a,b)) - (min (a,b)) = |.(a - b).| ; :: thesis: verum

end;

end;