:: deftheorem Def9 defines integral INTEGR18:def 9 :
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for a, b being 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'])) ) );