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;