Let the real numbers and the relations =, >, $\ge$ be defined as in this lecture PDF.
I want to show the following statement:
$$\forall x \in \mathbb{R}( x \ge 0 \wedge x \neq 0 \Longrightarrow x > 0).$$
From $ x \ge 0$ we get that for all $(q,q') \in x$ and $(r,r') \in 0$ the following holds: \begin{align*} r \le q'. \end{align*} From we $ x \neq 0$ we get that there exists $(u,u') \in x $ and $(v,v') \in 0$ such that $[u,u'] \cap [v,v']$ have no rational point in common. $\underline{\text{This implies } v' < u}$; whence $ 0 < x$.
I am not sure wether the underlined part is true.
The problem is that you have to justify From $x \neq 0$ we get that there exists $(u,u′) \in x$ and $(v,v′) \in 0$ such that $[u,u′] \cap [v,v′]$ have no rational point in common. as this is not an axiom used in your document for the construction of $\mathbb R$.
Let's do it.
By definition of $x \ge 0$, for all $(q,q^\prime) \in x$ you have $q^\prime \ge 0$, see page 59. This is also a consequence that the rational number $0$ is canonically identified as $\{(0,0)\}$, see page 57.
Now as $x \neq 0$, by page 58, you must have $(q,q^\prime) \cap \{0\} = \emptyset$. And this enables to conclude that $q > 0$ and therefore to $x >0$ using again page 58.
The important topic is that for a rational number $q$, the "associated" real number is the set $\{(q,q)\}$ as stated in page 57. In that case the "associated real number" contains a single ordered pair!