:: deftheorem defines division_of COUSIN:def 6 :
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
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] ) );