diff --git a/draft/draft.tex b/draft/draft.tex
index d20ca69..78069c9 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2036,35 +2036,67 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %	We have $(Fp_1)^\dagger\comp\sigma$.
 %\end{proof}
 \subsection{The concrete proof}
+%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
+%	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
+%	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
+%		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I1}
+%		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II1}
+%	\end{enumerate}
+%\end{lemma}
+%\begin{proof}
+%	 By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
+%	\begin{align}
+%		\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_11}\\
+%		\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_21}
+%	\end{align}
+%	(I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_21} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$. 
+%	Therefore:
+%	\begin{align*}
+%	\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
+%	=&\; \powf p_2\comp\sigma (x_2,x_1)\\
+%	\subseteq&\;\alpha(x_1)\\
+%	\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_11}}
+%	\end{align*}
+%	%
+%	(II): Analogously, from~\eqref{eq:alpha_x_11} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
+%	Therefore:
+%	\begin{align*}
+%	\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_21}}\\
+%	\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
+%	=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
+%	=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& 
+%	\end{align*}
+%	\qed
+%\end{proof}
 \begin{lemma}\label{lem:sim-opsim-inc}
-	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
+	In a category $\BC$, assuming that $F$ has a natural order structure $\appr$, and $\sigma\c R\to F R$ is witness for a symmetric relation $R$ to be an AM-simulation on $F$-coalgebra $(X,\alpha)$, then we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
-		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I}
-		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II}
+		\item $F p_1\comp F s\comp\sigma\comp s\appr F p_1\comp\sigma$\label{item:sim-opsim-inc:I}
+		\item $F p_2\comp\sigma\appr F p_2\comp F s\comp\sigma\comp s$\label{item:sim-opsim-inc:II}
 	\end{enumerate}
 \end{lemma}
 \begin{proof}
-	 By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
+	By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
 	\begin{align}
-		\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_1}\\
-		\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_2}
+		\alpha\comp p_1\appr&\;F p_1\comp\sigma,\label{eq:alpha_x_1}\\
+		F p_2\comp\sigma\appr&\;\alpha\comp p_2.\label{eq:alpha_x_2}
 	\end{align}
-	(I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_2} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$. 
+	(I): Since $R$ is symmetric and $\appr$ is a natural order structure, from \eqref{eq:alpha_x_2} we get $F p_2\comp\sigma\comp s\appr\alpha\comp p_2\comp s$. 
 	Therefore:
 	\begin{align*}
-	\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
-	=&\; \powf p_2\comp\sigma (x_2,x_1)\\
-	\subseteq&\;\alpha(x_1)\\
-	\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_1}}
+		F p_1\comp F s\comp\sigma\comp s=&\; F p_2\comp\sigma\comp s\\
+		\appr&\;\alpha\comp p_2\comp s\\
+		=&\;\alpha\comp p_1\\
+		\appr&\; F p_1\comp\sigma & \by{\eqref{eq:alpha_x_1}}
 	\end{align*}
 	%
-	(II): Analogously, from~\eqref{eq:alpha_x_1} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
+	(II): Analogously, from~\eqref{eq:alpha_x_1} since $R$ is symmetric and $\appr$ is a natural order structure, we get $\alpha\comp p_1\comp s\appr F p_1\comp\sigma\comp s$.
 	Therefore:
 	\begin{align*}
-	\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_2}}\\
-	\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
-	=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
-	=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& 
+		F p_2\comp\sigma\appr&\; \alpha\comp p_2 &\by{\eqref{eq:alpha_x_2}}\\
+		=&\; \alpha\comp p_1\comp s\\
+		\appr&\; F p_1\comp\sigma\comp s \\
+		=&\;F p_2\comp F s\comp\sigma\comp s.& 
 	\end{align*}
 	\qed
 \end{proof}
@@ -2163,7 +2195,7 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$.
 	\end{gather*}
 	Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
 	
-	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is reflexive, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
+	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
 \end{proof}
 
 \begin{prop}
@@ -2189,6 +2221,8 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$.
 	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.\qed
 \end{proof}
 
+
+
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}
 Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: