let f be PartFunc of REAL,REAL; :: thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)

let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)

let a, b be Real; :: thesis: ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A3: A = [.b,a.] ; :: thesis: - (integral (f,A)) = integral (f,a,b)
then A4: ( a1 = b & b1 = a ) by ;
now :: thesis: - (integral (f,A)) = integral (f,a,b)
per cases ( b < a or b = a ) by ;
suppose A5: b < a ; :: thesis: - (integral (f,A)) = integral (f,a,b)
then integral (f,a,b) = - (integral (f,['b,a'])) by Def4;
hence - (integral (f,A)) = integral (f,a,b) by A3, A5, Def3; :: thesis: verum
end;
suppose A6: b = a ; :: thesis: - (integral (f,A)) = integral (f,a,b)
A = [.(),().] by INTEGRA1:4;
then ( lower_bound A = b & upper_bound A = a ) by ;
then vol A = () - () by
.= 0 ;
then A7: integral (f,A) = 0 by INTEGRA4:6;
integral (f,a,b) = integral (f,['a,b']) by ;
hence - (integral (f,A)) = integral (f,a,b) by A3, A6, A7, Def3; :: thesis: verum
end;
end;
end;
hence - (integral (f,A)) = integral (f,a,b) ; :: thesis: verum