( max (a,b) >= a & a >= min (a,b) ) by XXREAL_0:17, XXREAL_0:25;
then max (a,b) >= min (a,b) by XXREAL_0:2;
then (max (a,b)) - (min (a,b)) >= (max (a,b)) - (max (a,b)) by XREAL_1:10;
hence not (max (a,b)) - (min (a,b)) is negative ; :: thesis: verum