theorem Th5: :: PDLAX:5

for a, b, c, d, e being Real
for f being PartFunc of REAL,REAL st 0 < e & 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 [.a,b.] holds
0 <= f . t ) & ( for t being Real st t in [.c,d.] holds
e <= f . t ) holds
( 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )