Priestley duality

Statement

Let $L$ be a bounded distributive lattice. A prime filter of $L$ is a filter $F$ with $0 \notin F$ such that $a \vee b \in F$ implies $a \in F$ or $b \in F$. Let $X_L$ be the set of prime filters of $L$, ordered by inclusion. Give $X_L$ the topology generated by the sets $\set{F : a \in F}$ and $\set{F : a \notin F}$ for $a \in L$. For a Priestley space $X$, let $\mathrm{ClopUp}(X)$ be the lattice of subsets of $X$ that are clopen upper sets. Its meet and join are intersection and union.

1. $X_L$ is a Priestley space, and the map $a \mapsto \set{F \in X_L : a \in F}$ is an isomorphism of bounded lattices from $L$ onto $\mathrm{ClopUp}(X_L)$.
2. For every Priestley space $X$, the map $x \mapsto \set{U \in \mathrm{ClopUp}(X) : x \in U}$ is a homeomorphism and order isomorphism from $X$ onto $X_{\mathrm{ClopUp}(X)}$.
3. These constructions extend to a dual equivalence of categories. On one side are the bounded distributive lattices with bounded lattice homomorphisms; on the other, the Priestley spaces with continuous order-preserving maps. A homomorphism $h \colon L \to M$ corresponds to the map $X_M \to X_L$, $G \mapsto h^{-1}(G)$.