for I being non empty closed_interval Subset of REAL
for D being Division of I
for T being Element of set_of_tagged_Division D holds rng T c= I