let A be 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 = max (rng (upper_volume (chi A,A),D2)) by INTEGRA1:def 19;
then 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:26;
len (upper_volume (chi A,A),D2) = len D2 by INTEGRA1:def 7;
then A3: j in dom D2 by A1, FINSEQ_3:31;
then A4: delta D2 = vol (divset D2,j) by A2, INTEGRA1:22;
assume D1 <= D2 ; :: thesis: delta D1 >= delta D2
then consider i being Element of NAT such that
A5: i in dom D1 and
A6: divset D2,j c= divset D1,i by A3, Th37;
A7: vol (divset D1,i) = (upper_volume (chi A,A),D1) . i by A5, INTEGRA1:22;
len (upper_volume (chi A,A),D1) = len D1 by INTEGRA1:def 7;
then i in dom (upper_volume (chi A,A),D1) by A5, FINSEQ_3:31;
then vol (divset D1,i) in rng (upper_volume (chi A,A),D1) by A7, FUNCT_1:def 5;
then delta D2 <= max (rng (upper_volume (chi A,A),D1)) by A4, A6, Th40, XXREAL_2:61;
hence delta D1 >= delta D2 by INTEGRA1:def 19; :: thesis: verum