let A be non empty 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 Element of REAL such that

A1: y in rng D by SUBSET_1:4;

consider n being Element of NAT such that

A2: n in dom D and

y = D . n by A1, PARTFUN1:3;

n in Seg (len D) by A2, FINSEQ_1:def 3;

then n in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

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 3;

then A3: (upper_volume ((chi (A,A)),D)) . n <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

vol (divset (D,n)) = (upper_volume ((chi (A,A)),D)) . n by A2, INTEGRA1:20;

then (upper_volume ((chi (A,A)),D)) . n >= 0 by INTEGRA1:9;

hence delta D >= 0 by A3; :: thesis: verum

let D be Division of A; :: thesis: delta D >= 0

consider y being Element of REAL such that

A1: y in rng D by SUBSET_1:4;

consider n being Element of NAT such that

A2: n in dom D and

y = D . n by A1, PARTFUN1:3;

n in Seg (len D) by A2, FINSEQ_1:def 3;

then n in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

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 3;

then A3: (upper_volume ((chi (A,A)),D)) . n <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

vol (divset (D,n)) = (upper_volume ((chi (A,A)),D)) . n by A2, INTEGRA1:20;

then (upper_volume ((chi (A,A)),D)) . n >= 0 by INTEGRA1:9;

hence delta D >= 0 by A3; :: thesis: verum