support (pfexp p) = {p} by Th43;
hence support (pfexp p) is 1 -element ; :: thesis: verum