theorem Th14: :: MESFUN15:12

for a, b, c, d being Real
for f being PartFunc of REAL,REAL st c <= d & [.c,d.] c= [.a,b.] & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonnegative holds
integral (f,c,d) <= integral (f,a,b)