theorem Th15: :: CAT_7:15

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