DEF-RCV. Converse Relation.
Let $R$ be a binary relation. The converse relation of $R$ is
\[R^{-1} = \{(y,x)\in\operatorname{ran}R\times\operatorname{dom}R:x\,R\,y\}.\]
PROP-RCV-DB.
For any binary relation $R$,
\[(R^{-1})^{-1} = R.\]
PROP-RCV-SYM.
A binary relation $R$ is symmetric if and only if $R=R^{-1}$.