Solution (source code)

= Solution

An <upper bound> of $S$ is an element $u\in A$ with $s\preceq u$ for every $s\in S$. It need not belong to $S$. A maximum, or <greatest element>, is an $m\in S$ with that same property. A <least upper bound> is an <upper bound> $\ell\in A$ satisfying $\ell\preceq u$ for every <upper bound> $u$.

\b[A maximum belongs to $S$; a <least upper bound> need not.] In a <partially ordered set>, an existing maximum is automatically the <least upper bound>, and the <antisymmetric relation> condition makes each unique.