support (pfexp (p |^ a)) = {p} by Th42;
hence ( not support (pfexp (p |^ a)) is empty & support (pfexp (p |^ a)) is trivial ) ; :: thesis: verum