let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A holds delta D >= 0
let D be Division of A; :: thesis: delta D >= 0
consider y being Real such that
A1: y in rng D by SUBSET_1:10;
consider n being Element of NAT such that
A2: ( n in dom D & y = D . n ) by A1, PARTFUN1:26;
A3: n in Seg (len D) by A2, FINSEQ_1:def 3;
vol (divset D,n) = (upper_volume (chi A,A),D) . n by A2, INTEGRA1:22;
then A4: (upper_volume (chi A,A),D) . n >= 0 by INTEGRA1:11;
n in Seg (len (upper_volume (chi A,A),D)) by A3, INTEGRA1:def 7;
then n in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . n in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
then (upper_volume (chi A,A),D) . n <= max (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 8;
hence delta D >= 0 by A4, INTEGRA1:def 19; :: thesis: verum