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 [.a,b.] = [.(inf [.a,b.]),(sup [.a,b.]).] by INTEGRA1:5;
then ( a = inf [.a,b.] & b = sup [.a,b.] ) by A1, INTEGRA1:6;
hence vol ['a,b'] = b - a by A1; :: thesis: verum