for C, D being with_identities CategoryStr st C ~= D & C is empty holds
D is empty