The text in Exercise 8.2 contains eight new definitions. Let $Δ$ be the corresponding environment. Rewrite the type in line (8) in such a manner that all definitions of $Δ$ have been unfolded.
Let's remind ourselves of the text in Exercise 8.2
The type in line (8) is
$$\textit{least-upper-bound}(S, p_6, 1)$$
Using (3) we have
$$\textit{upper-bound}(S, p_6, 1) \; \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \textit{upper-bound}(S, p_6, x))$$
Using (2) we have
$$ \forall x: \mathbb{R}.(x \in S \implies x \le 1) \; \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in S \implies y \le x) )$$
Note the use of $y$ to avoid clashing with $x$.
Using $(5)$ we have
$$\begin{gather*} \forall x: \mathbb{R}.(x \in \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \} \implies x \le 1) \\ \\ \land \\ \\ \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \} \implies y \le x) ) \end{gather*}$$
