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

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