theorem :: COUSIN:52

for I being non empty closed_interval Subset of REAL
for D being Division of I holds not set_of_tagged_Division D is empty by Th34;