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 )
A2: len D in dom D by FINSEQ_5:6;
assume A3: for i being Element of NAT st i in dom D holds
vol (divset D,i) <= 0 ; :: thesis: contradiction
A4: 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 A3;
hence vol (divset D,i) = 0 by INTEGRA1:11; :: thesis: verum

end;

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

proof

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

end;

A6: len D = 1

proof

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

end;

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