:: deftheorem Def3 defines tagged_division COUSIN:def 3 :
for I being non empty closed_interval Subset of REAL
for b₂ being object holds
( b₂ is tagged_division of I iff ex D being Division of I ex T being Element of set_of_tagged_Division D st b₂ = [D,T] );