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

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