The Stone prime filter theorem says that if a lattice filter and a lattice ideal of a distributive lattice are disjoint, then there is a prime filter of a distributive lattice such that
Equivalently, whenever , there is a prime filter containing and omitting .
For a prime filter , first suppose . If and , then and
so . Thus no prime filter above belongs to , and
Conversely, suppose . The lattice filter generated by is disjoint from the principal lattice ideal . Indeed, an intersection would give some with , whence and then , a contradiction. The Stone prime filter theorem therefore extends this filter to a prime filter that omits . Then , so .
We have proved, for every ,
which is the required identity