> 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.)