dom (C idval X) = X by Th131;
hence C idval X is empty ; :: thesis: verum