theorem :: INTEGRA9:33

for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
|||(f,f,A)||| >= 0 by INTEGRA2:32;