let A be non empty 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 that
A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) and
A2: for x being Real st x in A holds
f . x >= g . x ; :: thesis: integral f >= integral g
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 A2, A5, XREAL_1:48; :: thesis: verum

end;

( integral (f - g) = (integral f) - (integral g) & (f - g) | (A /\ A) is bounded ) by A1, Th33, RFUNCT_1:84;
hence integral f >= integral g by A4, Th32, XREAL_1:49; :: thesis: verum