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