let C, D be with_identities CategoryStr ; :: thesis: ( C ~= D & C is empty implies D is empty )
assume C ~= D ; :: thesis: ( not C is empty or D is empty )
then A1: card (Mor C) = card (Mor D) by Th14;
assume C is empty ; :: thesis: D is empty
hence D is empty by A1; :: thesis: verum