theorem Th85: :: CLASSES5:83

for C being CategorySet holds not C is empty