for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )