theorem :: FUZZY_6:2

for a, b being Real holds
( id REAL is_integrable_on ['a,b'] & (id REAL) | ['a,b'] is bounded )