let a, b be Real; :: thesis: vol ['(min (a,b)),(max (a,b))'] = |.(b - a).|

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

suppose A1: a <= b ; :: thesis: vol ['(min (a,b)),(max (a,b))'] = |.(b - a).|

then ( min (a,b) = a & max (a,b) = b ) by XXREAL_0:def 9, XXREAL_0:def 10;
then A2: vol ['(min (a,b)),(max (a,b))'] = b - a by Th5, XXREAL_0:25;
0 <= b - a by A1, XREAL_1:48;
hence vol ['(min (a,b)),(max (a,b))'] = |.(b - a).| by A2, ABSVALUE:def 1; :: thesis: verum

end;

suppose A3: not a <= b ; :: thesis: vol ['(min (a,b)),(max (a,b))'] = |.(b - a).|

then 0 <= a - b by XREAL_1:48;
then A4: a - b = |.(a - b).| by ABSVALUE:def 1
.= |.(b - a).| by COMPLEX1:60 ;
( min (a,b) = b & max (a,b) = a ) by A3, XXREAL_0:def 9, XXREAL_0:def 10;
hence vol ['(min (a,b)),(max (a,b))'] = |.(b - a).| by A4, Th5, XXREAL_0:17; :: thesis: verum

end;

end;