diff --git a/draft/draft.tex b/draft/draft.tex
index 159161d..3e200c5 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2248,6 +2248,13 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
+\begin{prop}
+	The following propositions hold:
+	\begin{itemize}
+		\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp\powf\pi_2\comp(\powf\pi_1)^\op$
+		\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp\powf\pi_1\comp(\powf\pi_2)^\op$
+	\end{itemize}
+\end{prop}
 \end{document}