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