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:
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 ;
hence (f - g) . x >= 0 by ; :: thesis: verum
end;
( integral (f - g) = () - () & (f - g) | (A /\ A) is bounded ) by ;
hence integral f >= integral g by ; :: thesis: verum