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;