let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A, REAL
for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f | A is bounded_below holds
lower_sum f,D2 >= lower_sum f,D1
let f be Function of A, REAL ; :: thesis: for S being non empty Division of A
for D1, D2 being Element of S st D1 <= D2 & f | A is bounded_below holds
lower_sum f,D2 >= lower_sum f,D1
let S be non empty Division of A; :: thesis: for D1, D2 being Element of S st D1 <= D2 & f | A is bounded_below holds
lower_sum f,D2 >= lower_sum f,D1
let D1, D2 be Element of S; :: thesis: ( D1 <= D2 & f | A is bounded_below implies lower_sum f,D2 >= lower_sum f,D1 )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_below ; :: thesis: lower_sum f,D2 >= lower_sum f,D1
len D1 in dom D1

proof

len D1 in Seg (len D1) by FINSEQ_1:5;
hence len D1 in dom D1 by FINSEQ_1:def 3; :: thesis: verum

end;

then (PartSums (lower_volume f,D1)) . (len D1) <= (PartSums (lower_volume f,D2)) . (indx D2,D1,(len D1)) by A1, A2, Th43;
then lower_sum f,D1 <= (PartSums (lower_volume f,D2)) . (indx D2,D1,(len D1)) by Th45;
then lower_sum f,D1 <= (PartSums (lower_volume f,D2)) . (len D2) by A1, Th46;
hence lower_sum f,D2 >= lower_sum f,D1 by Th45; :: thesis: verum