theorem Th6: :: PDLAX:6

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