theorem Th3: :: PDLAX:3

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