for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for D being Division of I
for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )