Description: Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)