let a, b be Real; :: 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 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; :: thesis: verum