Description: When ph is substituted for ps , this statement expresses that weak nonfreeness implies the "exists" form of nonfreeness. (Contributed by BJ, 9-Dec-2023)