let a, b be Real; :: thesis: ( a <= b implies integral ((Cst 1),a,b) = b - a )
assume a <= b ; :: thesis: integral ((Cst 1),a,b) = b - a
then [.a,b.] = ['a,b'] by INTEGRA5:def 3;
then reconsider A = [.a,b.] as non empty closed_interval Subset of REAL ;
( upper_bound A = b & lower_bound A = a ) by Th37;
then A1: vol A = b - a by INTEGRA1:def 5;
( integral ((Cst 1),a,b) = integral ((Cst 1),A) & (Cst 1) || A = chi (A,A) ) by Th36, INTEGRA5:19;
hence integral ((Cst 1),a,b) = b - a by A1, INTEGRA4:2; :: thesis: verum