support (pfexp p) = {p} by Th43;
hence ( not support (pfexp p) is empty & support (pfexp p) is trivial ) ; :: thesis: verum