:: deftheorem defines division_of COUSIN:def 6 :
for I being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I,REAL
for TD being tagged_division of I,jauge
for b₄ being Division of I holds
( b₄ = division_of TD iff ex D being Division of I ex T being Element of set_of_tagged_Division D st
( b₄ = D & TD = [D,T] ) );