Solution (source code)

= Solution

For a prime filter $P\in\widehat H$, first suppose $a\Rightarrow b\in P$. If $Q\supseteq P$ and $a\in Q$, then $a\Rightarrow b\in Q$ and
$$
a\wedge(a\Rightarrow b)\leq b,
$$
so $b\in Q$. Thus no prime filter above $P$ belongs to $a^*\setminus b^*$, and
$$
P\notin\uparrow(a^*\setminus b^*).
$$

Conversely, suppose $a\Rightarrow b\notin P$. The <lattice filter> generated by $P\cup\{a\}$ is disjoint from the principal <lattice ideal> $\mathord\downarrow b$. Indeed, an intersection would give some $p\in P$ with $p\wedge a\leq b$, whence $p\leq a\Rightarrow b$ and then $a\Rightarrow b\in P$, a contradiction. The <Stone prime filter theorem> therefore extends this filter to a prime filter $Q\supseteq P$ that omits $b$. Then $Q\in a^*\setminus b^*$, so $P\in\uparrow(a^*\setminus b^*)$.

We have proved, for every $P$,
$$
P\in(a\Rightarrow b)^*
\quad\Longleftrightarrow\quad
P\notin\uparrow(a^*\setminus b^*),
$$
which is the required identity
$$
(a\Rightarrow b)^*=\bigl(\uparrow(a^*\setminus b^*)\bigr)^{\mathcal C}.
$$