> I thought Michael was taking a different approach than the one I suggested: proving that \$$\Phi(x',y') = \text{true}\$$ if \$$\Phi(x,y) = \text{true}\$$, \$$x' \le x\$$ and \$$y \le y'\$$. This uses the 'original' definition of enriched profunctor, which I expanded to a lengthier definition in the theorem in [Lecture 56](https://forum.azimuthproject.org/discussion/2280/lecture-56-chapter-4-feasibility-relations/p1).

Ah, sure I see that we can say \$$\Phi\$$ is a feasibility relation if it obeys the axiom:

$x' \le x \text{ and } y \le y' \text{ and } \Phi(x,y) \text{ implies } \Phi(x',y')$

Michael's proof certainly works, I was just thrown off because I had assumed he was going to prove parts (1) and (2) like you outlined. My mistake!