+$$
+\begin{cases}
+ L \haspatch \p : & C \haspatch \p \\
+ L \nothaspatch \p : & C \nothaspatch \p
+\end{cases}
+$$
+\proofstarts
+
+Firstly, if $L \haspatch \p$, $\exists_{F \in \py} F \le L$
+and this $F$ is also $\le C$
+so $C \zhaspatch \p \implies C \haspatch \p$.
+We will prove $\zhaspatch$
+
+We need to consider $D \in \py$.