let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A st vol A <> 0 holds
ex i being Element of NAT st
( i in dom D & vol (divset D,i) > 0 )
let D be Division of A; :: thesis: ( vol A <> 0 implies ex i being Element of NAT st
( i in dom D & vol (divset D,i) > 0 ) )
assume A1: vol A <> 0 ; :: thesis: ex i being Element of NAT st
( i in dom D & vol (divset D,i) > 0 )
assume A2: for i being Element of NAT st i in dom D holds
vol (divset D,i) <= 0 ; :: thesis: contradiction
A3: for i being Element of NAT st i in dom D holds
vol (divset D,i) = 0

proof

let i be Element of NAT ; :: thesis: ( i in dom D implies vol (divset D,i) = 0 )
assume i in dom D ; :: thesis: vol (divset D,i) = 0
then vol (divset D,i) <= 0 by A2;
hence vol (divset D,i) = 0 by INTEGRA1:11; :: thesis: verum

end;

A4: for i being Element of NAT st i in dom D holds
sup (divset D,i) = lower_bound (divset D,i)

proof

let i be Element of NAT ; :: thesis: ( i in dom D implies sup (divset D,i) = lower_bound (divset D,i) )
assume i in dom D ; :: thesis: sup (divset D,i) = lower_bound (divset D,i)
then vol (divset D,i) = 0 by A3;
then (upper_bound (divset D,i)) - (lower_bound (divset D,i)) = 0 by INTEGRA1:def 6;
hence sup (divset D,i) = lower_bound (divset D,i) ; :: thesis: verum

end;

A5: len D in dom D by FINSEQ_5:6;
len D = 1

proof

assume A6: len D <> 1 ; :: thesis: contradiction
then A7: ( lower_bound (divset D,(len D)) = D . ((len D) - 1) & upper_bound (divset D,(len D)) = D . (len D) ) by A5, INTEGRA1:def 5;
A8: ( (len D) - 1 in dom D & (len D) - 1 in NAT ) by A5, A6, INTEGRA1:9;
len D < (len D) + 1 by NAT_1:13;
then (len D) - 1 < len D by XREAL_1:21;
then lower_bound (divset D,(len D)) < upper_bound (divset D,(len D)) by A5, A7, A8, SEQM_3:def 1;
hence contradiction by A4, A5; :: thesis: verum

end;

then ( lower_bound (divset D,(len D)) = lower_bound A & upper_bound (divset D,(len D)) = D . (len D) ) by A5, INTEGRA1:def 5;
then ( lower_bound (divset D,(len D)) = lower_bound A & upper_bound (divset D,(len D)) = upper_bound A ) by INTEGRA1:def 2;
then upper_bound A = (lower_bound A) + 0 by A4, A5;
then (upper_bound A) - (lower_bound A) = 0 ;
hence contradiction by A1, INTEGRA1:def 6; :: thesis: verum