theorem Th2: :: INTEGRA3:2

for A being non empty closed_interval Subset of REAL
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 )