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

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

end;

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;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

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;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