for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I holds len (tagged_of TD) = len (division_of TD)