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)\\).

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)\\).