> 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!