Solution (source code)

= Solution

The <Stone prime filter theorem> says that if a <lattice filter> $F$ and a <lattice ideal> $I$ of a <distributive lattice> are disjoint, then there is a <prime filter of a distributive lattice> $P$ such that
$$
F\subseteq P
\quad\text{and}\quad
P\cap I=\varnothing.
$$
Equivalently, whenever $a\nleq b$, there is a prime filter containing $a$ and omitting $b$.