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