theorem Th4: :: PDLAX:4

for a, b, c, d, e being Real
for f being PartFunc of REAL,REAL st a <= b & c <= d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.c,d.] holds
e <= f . t ) holds
e * (d - c) <= integral (f,c,d)