OK I think I see the connection now.

We're trying to prove this theorem:

> the definition of feasibility relation says that
>
> $\text{if } (x,y) \le (x',y') \text{ in } X^{\text{op}} \times Y, \text{ then }\Phi(x,y) \text{ implies } \Phi(x',y') .$
>
> this one condition is equivalent to two conditions:
>
> 1. if \$$x' \le x \$$ in \$$X\$$, then \$$\Phi(x,y) \$$ implies \$$\Phi(x',y)\$$ for all \$$y \in Y\$$,
>
> 2. if \$$y \le y'\$$ in \$$Y\$$, then \$$\Phi(x,y) \$$ implies \$$\Phi(x,y')\$$ for all \$$x \in X\$$.

Showing that the one condition implies the two conditions is trivial. But what about the other way round?

Suppose we have the two conditions and also \$$(x,y) \le (x',y')\$$, ie \$$x'\le x\$$ and \$$y\le y'\$$.

We have a choice of two routes here.

One route goes: \$$(x,y) \le (x',y) \le (x',y')\$$, so \$$\Phi(x, y)\$$ implies \$$\Phi(x',y)\$$ by condition
1, which implies \$$\Phi(x',y')\$$ by condition 2.

The other route goes: \$$(x,y) \le (x,y') \le (x',y')\$$, so \$$\Phi(x, y)\$$ implies \$$\Phi(x,y')\$$ by condition
2, which implies \$$\Phi(x',y')\$$ by condition 1.

So we can prove our theorem in two distinct ways corresponding to the two ways of "factorising" \$$(x,y) \le (x',y')\$$.