:: deftheorem defines integral INTEGRA5:def 2 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds integral (f,A) = integral (f || A);