A D4424: Binary endorelation $B = (X \times Y, R)$ is transitive if and only if \begin{equation} \forall \, x, y, z \in X \left( x R y, y R z \quad \implies \quad x R z \right) \end{equation}