let p be Prime; :: thesis: support (ppf p) = {p}
support (pfexp p) = {p} by NAT_3:43;
hence support (ppf p) = {p} by NAT_3:def 9; :: thesis: verum