 Fixed point theorem.  Let \(\tau\) be a monotone operator on a chain complete partial order (henceforth ccpo). Then \(\tau\) has a least fixed point, that is, there is a least f such that \(\tau(f) = f\). 