does it work?

draft/draft.tex

@@ -2149,6 +2149,17 @@ 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}
+\begin{prop}
+	Assuming that for a relator $\relar$ over $F\c\Set\to\Set$, $\hat{\relar}$ is difunctionally functorial, then $\relar$ is also difunctionally functorial, and vice-versa.
+\end{prop}
+\begin{proof}
+	$\hat{\relar}$ being difunctionally functorial means that for every functions $f\c X\to FX$ and $g\c Y\to FY$, we have $\hat{\relar}(g^\op\comp f)=(Fg)^\op\comp Ff$. It is equivalent with the both following conditions being true:
+	\begin{itemize}
+		\item ${\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$, or $({\relar}(f^\op\comp g))^\op\leq(Fg)^\op\comp Ff$
+		\item ${\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$ and $({\relar}(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$
+	\end{itemize}
+	The proof from right to left is obvious. For the other direction we assume that $\hat{\relar}$ is difunctinally functorial. Then we have $\hat{\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$ and $\hat{\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$. The earlier gives the first item, and the later gives the second item.
+\end{proof}
 \end{document}