Puzzle 174:
Given \\(g : Y -> X\\) and \\(\Psi(x,y) = x \le g(y)\\), we must show that \\(\Psi\\) is a feasibility relation.
\\( \Psi \\) is a feasibility relation if and only if
\\[\forall x',x : X, y,y' : Y, x'\le x, y \le y', \Psi(x,y) \to \Psi(x',y')\\]
\\(\Psi(x,y)\\) equals, by the definition of Psi:
\\[x \le g(y)\\]
By transitivity and \\(x\le x'\\):
\\[x'\le g(y)\\]
By monotonicity we have
\\[y\le y' \to g(y)\le g(y')\\]
and so
\\[\to x'\le g(y')\\]
which by definition of \\(\Psi\\), equals \\(\Psi(x',y')\\)
Therefor,
\\[\Psi(x,y) \to \Psi(x',y')\\]
QED.