let a, b be Real; vol ['(min (a,b)),(max (a,b))'] = |.(b - a).|
per cases
( a <= b or not a <= b )
;
suppose A1:
a <= b
;
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;
verum end; end;