Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.
Proof of Proposition 5.1.4.1.2.
Item 1: Characterisations
We claim that Item (a) and Item (b) are indeed equivalent: - Item (a)$\implies $Item (b): Let $\webleft (b,b'\webright )\in B\times B$. We need to show that
\[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]
i.e. that if there exists some $a\in A$ such that $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, then $b=b'$. But since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, we have both $a\sim _{R}b$ and $a\sim _{R}b'$ at the same time, which implies $b=b'$ since $R$ is functional.
- Item (b)$\implies $Item (a): Suppose that we have $a\sim _{R}b$ and $a\sim _{R}b'$ for $b,b'\in B$. We claim that $b=b'$:
- Since $a\sim _{R}b$, we have $b\sim _{R^{\dagger }}a$.
- Since $R\mathbin {\diamond }R^{\dagger }\subset \chi _{B}$, we have
\[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]
and since $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, it follows that $\webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )=\mathsf{true}$, and thus $\chi _{B}\webleft (b,b'\webright )=\mathsf{true}$ as well, i.e. $b=b'$.
