let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st D1 <= D2 holds
delta D1 >= delta D2
let D1, D2 be Division of A; :: thesis: ( D1 <= D2 implies delta D1 >= delta D2 )
delta D2 in rng (upper_volume ((chi (A,A)),D2)) by XXREAL_2:def 8;
then consider j being Element of NAT such that
A1: j in dom (upper_volume ((chi (A,A)),D2)) and
A2: delta D2 = (upper_volume ((chi (A,A)),D2)) . j by PARTFUN1:3;
len (upper_volume ((chi (A,A)),D2)) = len D2 by INTEGRA1:def 6;
then A3: j in dom D2 by A1, FINSEQ_3:29;
then A4: delta D2 = vol (divset (D2,j)) by A2, INTEGRA1:20;
assume D1 <= D2 ; :: thesis: delta D1 >= delta D2
then consider i being Nat such that
A5: i in dom D1 and
A6: divset (D2,j) c= divset (D1,i) by A3, INTEGRA2:37;
A7: vol (divset (D1,i)) = (upper_volume ((chi (A,A)),D1)) . i by A5, INTEGRA1:20;
len (upper_volume ((chi (A,A)),D1)) = len D1 by INTEGRA1:def 6;
then i in dom (upper_volume ((chi (A,A)),D1)) by A5, FINSEQ_3:29;
then vol (divset (D1,i)) in rng (upper_volume ((chi (A,A)),D1)) by A7, FUNCT_1:def 3;
then delta D2 <= max (rng (upper_volume ((chi (A,A)),D1))) by A4, A6, INTEGRA2:38, XXREAL_2:61;
hence delta D1 >= delta D2 ; :: thesis: verum