let A be closed-interval Subset of REAL ; :: thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) holds
integral f >= integral g
let f, g be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) implies integral f >= integral g )
assume A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) ) ; :: thesis: integral f >= integral g
then A2: ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) by Th33;
A3: dom (f - g) = A by FUNCT_2:def 1;
A4: for x being Real st x in A holds
(f - g) . x >= 0

proof

let x be Real; :: thesis: ( x in A implies (f - g) . x >= 0 )
assume A5: x in A ; :: thesis: (f - g) . x >= 0
then (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;
hence (f - g) . x >= 0 by A1, A5, XREAL_1:50; :: thesis: verum

end;

(f - g) | (A /\ A) is bounded by A1, RFUNCT_1:101;
then (integral f) - (integral g) >= 0 by A2, A4, Th32;
hence integral f >= integral g by XREAL_1:51; :: thesis: verum