let a, b, c, d be Real; :: thesis: 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)
let f, g be PartFunc of REAL,REAL; :: thesis: ( 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 ) implies integral (f,c,d) <= integral (g,c,d) )
assume A1: ( 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 ) ) ; :: thesis: integral (f,c,d) <= integral (g,c,d)
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then A3: ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A1, INTEGRA5:10, INTEGRA5:11;
A4: ( g | ['a,b'] is bounded & g is_integrable_on ['a,b'] ) by A1, A2, INTEGRA5:10, INTEGRA5:11;
then A5: integral ((g - f),c,d) = (integral (g,c,d)) - (integral (f,c,d)) by A1, A2, A3, INTEGRA6:24;
A6: ( a <= c & c <= b & a <= d & d <= b ) by A1, XXREAL_1:1;
then A7: ['c,d'] c= dom f by A1, A2, A3, INTEGRA6:18;
A8: ['c,d'] c= dom g by A1, A2, A4, A6, INTEGRA6:18;
A9: dom (g - f) = (dom f) /\ (dom g) by VALUED_1:12;
A11: (g - f) | ['a,b'] = (g | ['a,b']) - (f | ['a,b']) by RFUNCT_1:47;
for t being Real st t in [.c,d.] holds
0 <= (g - f) . t

proof

let t be Real; :: thesis: ( t in [.c,d.] implies 0 <= (g - f) . t )
assume A12: t in [.c,d.] ; :: thesis: 0 <= (g - f) . t
then t in ['c,d'] by A1, INTEGRA5:def 3;
then A13: t in dom (g - f) by A7, A8, A9, XBOOLE_0:def 4;
(f . t) - (f . t) <= (g . t) - (f . t) by A1, A12, XREAL_1:9;
hence 0 <= (g - f) . t by A13, VALUED_1:13; :: thesis: verum

end;

then 0 <= (integral (g,c,d)) - (integral (f,c,d)) by A1, A5, A9, A11, Th2, XBOOLE_1:19;
then 0 + (integral (f,c,d)) <= ((integral (g,c,d)) - (integral (f,c,d))) + (integral (f,c,d)) by XREAL_1:7;
hence integral (f,c,d) <= integral (g,c,d) ; :: thesis: verum