let A be non empty closed_interval Subset of REAL; for D being Division of A holds delta D >= 0
let D be Division of A; 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; verum