theorem :: CAT_8:11

for C1, C2 being category st C1 ~= C2 holds
( C1 is empty iff C2 is empty )