theorem Lm22c: :: FUZZY_7:38

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real st a < b & b < c & c < d holds
( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded )