Maximum function

context	$X$
context	$\le$ … non-strict partial order over $X$

definiendum	$\mathrm{max}:X\times X\to X$
definiendum	$\mathrm{max}(x,y) := \begin{cases} x & \mathrm{if}\ y\le x\\\\ y & \mathrm{else} \end{cases}$