:: deftheorem Def2 defines tagged_of COUSIN2:def 5 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A
for b₃ being non empty non-decreasing FinSequence of REAL holds
( b₃ = tagged_of TD iff ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₃ = T & TD = [D,T] ) );