for a, t being Real
for f, g being PartFunc of REAL,REAL st a <= t & ['a,t'] c= dom f & f is_integrable_on ['a,t'] & f | ['a,t'] is bounded & ['a,t'] c= dom g & g is_integrable_on ['a,t'] & g | ['a,t'] is bounded & ( for x being Real st x in ['a,t'] holds
f . x <= g . x ) holds
integral (f,a,t) <= integral (g,a,t)