theorem Th41: :: COUSIN2:47

for I being non empty closed_interval Subset of REAL
for f being bounded integrable Function of I,REAL
for epsilon being Real st not I is trivial & 0 < epsilon holds
ex D being Division of I st
( D . 1 <> lower_bound I & upper_sum (f,D) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,D) & (upper_sum (f,D)) - (lower_sum (f,D)) < epsilon )