:: deftheorem defines non-empty CLASSES5:def 29 :
for C being quintuple StrCategory-like Category-like set holds
( C is non-empty iff not Obj C is empty );