let a, b be real number ; :: thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a)

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

suppose A1: a <= b ; :: thesis: vol ['(min (a,b)),(max (a,b))'] = abs (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:50;
hence vol ['(min (a,b)),(max (a,b))'] = abs (b - a) by A2, ABSVALUE:def 1; :: thesis: verum

end;

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

then 0 <= a - b by XREAL_1:50;
then A4: a - b = abs (a - b) by ABSVALUE:def 1
.= abs (b - a) by COMPLEX1:146 ;
( 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))'] = abs (b - a) by A4, Th5, XXREAL_0:17; :: thesis: verum

end;

end;