theorem Th12: :: MESFUN15:10

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