let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real holds integral (f,b,a) = - (integral (f,a,b))
let a, b be Real; :: thesis: integral (f,b,a) = - (integral (f,a,b))

per cases ( a <= b or a > b ) ;

suppose a <= b ; :: thesis: integral (f,b,a) = - (integral (f,a,b))

then A1: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then integral (f,['a,b']) = integral (f,a,b) by INTEGRA5:19;
hence integral (f,b,a) = - (integral (f,a,b)) by A1, INTEGRA5:20; :: thesis: verum

end;

suppose a > b ; :: thesis: integral (f,b,a) = - (integral (f,a,b))

then A2: ['b,a'] = [.b,a.] by INTEGRA5:def 3;
then - (integral (f,['b,a'])) = integral (f,a,b) by INTEGRA5:20;
hence integral (f,b,a) = - (integral (f,a,b)) by A2, INTEGRA5:19; :: thesis: verum

end;

end;