Left-Division in Rel

I got up earlier than expected and had a little bit of time to do a small exercise. Below is a proof of the universal property of left-division in Rel:

The power of classical logic is essential to this proof. But there is a constructive proof in AoPA (for right-division).

--
I have to think more thoroughly about what happens in the proof...