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