support (pfexp (p |^ a)) = {p} by Th42;
hence support (pfexp (p |^ a)) is 1 -element ; :: thesis: verum