for A being non empty closed_interval Subset of REAL
for D being Division of A holds D in set_of_tagged_Division D