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 4;
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 6;
( 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