begin
begin
begin
Lm1:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
::
deftheorem Def4 defines
integral INTEGRA5:def 4 :
for a, b being real number
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'])) ) );