The fundamental theorem of compact semilattices

Bounded-complete domains, or bc-domains, are an amazingly rich kind of continuous domains. They form a Cartesian-closed category, and they are the densely injective topological spaces, among other properties. One characterization of bc-domains which I have not included in the book is that they are related in a very precise sense to Lawson semilattices, namely to compact semilattices with small semilattices. This is the fundamental theorem of compact semilattices, which I will (re)prove by relying a lot on the theory of compact pospaces and stably compact spaces: see the full post.