+Consider $D \neq C, M \nothaspatch P, D \isin Y$:
+$D \le Y$ so $D \le C$.
+$D \not\isin M$ so by $\merge$, $D \isin C$. OK.
+
+Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
+$D \not\le Y$. If $D \le X$ then
+$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
+Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
+Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
+
+Consider $D \neq C, M \haspatch P, D \isin Y$:
+$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
+and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
+Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
+
+Consider $D \neq C, M \haspatch P, D \not\isin Y$:
+By $\merge$, $D \not\isin C$. OK.
+
+$\qed$
+