Solution (source code)

= Solution

We prove the result <algebraic partially ordered sets are continuous> directly from the definitions. First, $a\ll b$ implies $a\leq b$, by applying the <way-below relation> to the singleton <directed set> $\{b\}$. Also,
$$
a\ll b\leq c\quad\Longrightarrow\quad a\ll c:
$$
if $c\leq\sup D$, then $b\leq\sup D$, so the witness required for $a\ll b$ also works for $a\ll c$.

Fix $x$ and put
$$
K_x=\{k:k\leq x,\ k\ll k\},\qquad A_x=\{a:a\ll x\}.
$$
By algebraicity, $K_x$ is a <directed set> with <least upper bound> $x$. Every $k\in K_x$ satisfies $k\ll k\leq x$, hence $k\ll x$. Thus $K_x\subseteq A_x\subseteq\{a:a\leq x\}$.

To prove that $A_x$ is a <directed set>, take $a,b\in A_x$. Applying $a\ll x$ and $b\ll x$ to $x=\sup K_x$ gives $k_a,k_b\in K_x$ such that $a\leq k_a$ and $b\leq k_b$. Directedness of $K_x$ gives $k\in K_x$ above both. Since $k\in A_x$, it is the required common <upper bound> inside $A_x$. With the usual nonempty convention, $A_x$ is nonempty since it contains $K_x$.

By directed completeness $A_x$ has a <least upper bound>. The inclusions above give
$$
x=\sup K_x\leq\sup A_x\leq x,
$$
so
$$
\boxed{A_x\text{ is directed and }x=\sup A_x;\text{ hence the order is continuous}.}
$$
The same proof handles the paper's literal empty-set convention. If $K_x=\varnothing$, then $x=\sup\varnothing=\bot$, and the defining implication for $a\ll x$, applied to $D=K_x$, shows that $A_x$ must also be empty. Its <least upper bound> is again $x$. If $K_x$ is nonempty, the argument already given applies without change.