> but by the definition of closed this is true if and only if
>
> $x \otimes (x \multimap y) \otimes (y \multimap z) \le z.$

It's interesting to note that by the definition of being closed, this is the same as \$$(x \multimap y) \otimes (y \multimap z) \le (x \multimap z)\$$, which is exactly the logical rule of [hypothetical syllogism](https://en.wikipedia.org/wiki/Hypothetical_syllogism). (Alternatively, it's the same shape as composing two arrows.)