+$$
+\proof{
+Trivial for $C \in \set P$. For $C \not\in \set P$,
+$\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
+So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
+Consider some $E \in \pendsof{A}{\set P}$. If $\exists_{B,F}$ as
+specified, then either $F$ is going to be in our result and
+disqualifies $E$, or there is some other $F'$ (or, eventually,
+an $F''$) which disqualifies $F$.
+Otherwise, $E$ meets all the conditions for $\pends$.
+}