let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st vol A = 0 holds
len D = 1
let D be Division of A; :: thesis: ( vol A = 0 implies len D = 1 )
assume that
A1: vol A = 0 and
A2: len D <> 1 ; :: thesis: contradiction
rng D <> {} ;
then A3: 1 in dom D by FINSEQ_3:32;
then A4: 1 <= len D by FINSEQ_3:25;
then A5: len D in dom D by FINSEQ_3:25;
D . 1 in A by A3, INTEGRA1:6;
then A6: lower_bound A <= D . 1 by INTEGRA2:1;
1 < len D by A2, A4, XXREAL_0:1;
then A7: D . 1 < D . (len D) by A3, A5, SEQM_3:def 1;
(upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def 5;
hence contradiction by A7, A6, INTEGRA1:def 2; :: thesis: verum