prop

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}