diff --git a/draft/draft.tex b/draft/draft.tex
index 591bd2a..f6e9e5a 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2150,7 +2150,7 @@ then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in
 \begin{cor}
 	Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice.
 \end{cor}
-\subsection{Egli-Milner relator}
+\subsection{Egli-Milner relator and Barr relators}
 \begin{definition}
 	We call the map $\emre\c\rel\to\rel$ the Egli-Milner $\powf$-relator, whenever for every relation $r\c X\rto Y$ it is defined as follows:
 	\begin{gather*}
@@ -2187,20 +2187,29 @@ Egli-Milner relator is not sound or complete, although its symmetrization is sou
 		&\iff S\;(\powf g)^\op\comp\powf f\;T
 	\end{align*}\qed
 \end{proof}
-The symmetrization of the Egli-Milner relator is a Barr-relator. Barr-relator is a generalization of the Egli-Milner relator, where the functor is generalized.
 
 \begin{prop}
-	Assuming that $r\c X\rto Y$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then $\appr_{X};\hat{\emre};\appr_{Y}=\appr_{X};\hat{\emre}$ and $\appr_{X};\hat{\emre}=\hat{\emre};\appr_{Y}$.
+	Assuming that $r\c X\rto Y$, then $\subseteq;\hat{\emre};\subseteq=\subseteq;\hat{\emre}$ and $\subseteq;\hat{\emre}=\hat{\emre};\subseteq$.
 \end{prop}
 
+Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
+
 \begin{definition}
-	A relator over a functor $F$ is a Barr-relator, shown by $\bar{F}$, iff for a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
+	A relator over a functor $F$ is a Barr relator, shown by $\bar{F}$, iff for a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
 	\begin{gather*}
 		\bar{F}r=F\pi_2\comp(F\pi_1)^\op
 	\end{gather*}
 \end{definition}
+
 \begin{prop}
-	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr-relator.
+	$\hat{L}$ is a Barr relator.
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+
+\begin{prop}
+	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
 \end{prop}
 \begin{proof}
 	\todo{Finish.}