let a, b be real number ; :: thesis: vol ['(min a,b),(max a,b)'] = abs (b - a)
A1: ( min a,b <= a & a <= max a,b ) by XXREAL_0:17, XXREAL_0:25;

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

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

end;

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

then A5: ( min a,b = b & max a,b = a ) by XXREAL_0:def 9, XXREAL_0:def 10;
0 <= a - b by A4, XREAL_1:50;
then a - b = abs (a - b) by ABSVALUE:def 1
.= abs (b - a) by COMPLEX1:146 ;
hence vol ['(min a,b),(max a,b)'] = abs (b - a) by A1, A5, Th5; :: thesis: verum

end;

end;