:: deftheorem Def4 defines integral INTEGRA5:def 4 :
for a, b being Real
for f being PartFunc of REAL,REAL holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );