theorem :: COUSIN:58

for I being non empty closed_interval Subset of REAL
for D being Division of I
for T being Element of set_of_tagged_Division D holds not T is empty