173: I agree that the reference to Proposition 1.81 in Theorem 1.88 seems circular, and I think I've found a way to fix it:

By the logic of the proof up to the point in question, we have \$$g(f(p_0)) \leq g(q_0)\$$. From the definition of \$$f\$$, we have \$$g(f(p_0)) = g(\bigwedge \\{ q \in Q: \; p_0 \leq g(q) \\})\$$. But \$$g\$$ preserves meets, so \$$g(f(p_0)) = g(\bigwedge \\{ q \in Q: \; p_0 \leq g(q) \\}) = \bigwedge g(\\{ q \in Q: \; p_0 \leq g(q) \\})\$$. Then \$$p_0\$$ is obviously a lower bound for \$$g(\\{ q \in Q: \; p_0 \leq g(q) \\})\$$, so we get the desired inequality \$$p_0 \leq g(f(p_0)) \leq g(q_0)\$$.