let A be non empty 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:9; :: 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 5;
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:19;
assume A8: len D <> 1 ; :: thesis: contradiction
then A9: upper_bound (divset (D,(len D))) = D . (len D) by A2, INTEGRA1:def 4;
A10: (len D) - 1 in dom D by A2, A8, INTEGRA1:7;
lower_bound (divset (D,(len D))) = D . ((len D) - 1) by A2, A8, INTEGRA1:def 4;
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 4;
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 4;
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 5; :: thesis: verum