:: deftheorem Def1 defines tagged_divs COUSIN2:def 4 :
for A being non empty closed_interval Subset of REAL
for b₂ being set holds
( b₂ = tagged_divs A iff for x being set holds
( x in b₂ iff x is tagged_division of A ) );