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