theorem Th17: :: MESFUN14:17

for A being non empty closed_interval Subset of REAL
for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds
( delta T is 0 -convergent & delta T is non-zero )