let a, b be Real; ( a <= b implies vol ['a,b'] = b - a )
assume
a <= b
; vol ['a,b'] = b - a
then A1:
['a,b'] = [.a,b.]
by INTEGRA5:def 3;
then A2:
[.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).]
by INTEGRA1:4;
then
a = lower_bound [.a,b.]
by A1, INTEGRA1:5;
hence
vol ['a,b'] = b - a
by A1, A2, INTEGRA1:5; verum