Hi everybody I'd like to know if the next argument is sound.
Definitions: A real number x is said to be positive if can be written as a formal limit of a Cauchy sequence of rational numbers $(x_n)$ which is positively bounded away from zero, i.e., $\,x_n\ge c$ for each n, where $c$ is a positive rational number.
Proposition: Given any two real numbers $x<y$, we can find a rational number $q$ such that $x<q<y$.
Proof:
It will suffice to find two rational numbers such that $x\le q_1<q_2 \le y$, because we can define $q= \frac{q_1+q_2}{2}$ and we're done.
Let $(a_n)_{n=1}^{\infty}$, $(b_n)_{n=1}^{\infty}$ be Cauchy sequences such that their formal limits are the real number $y$ and $x$ respectively.
Since $y-x$ is a positive real number there exists a positive rational number $c$ such that $y-x>c$. Let $\,\epsilon= c/6$. Then there exists sufficient large $N_{\epsilon}\in \mathbb{N}$ such that: $|a_n-a_m|\le \epsilon$, $|b_n-b_m|\le \epsilon$ occurs simultaneously for all $n,m\ge N_{\epsilon}$. Moreover the sequence $(a_n-b_n)$ is eventually greater than $c$, let $M$ be the natural number such that $ a_n-b_n \ge c$ for all $n\ge M$. We set $N =max(N_{\epsilon}, M)$. Now let us fix some $n_0$ such that $n_0\ge N$. Then clearly $|y - a_{n_0}|\le c/6$ and $|x-b_{n_0}|\le c/6$ at the same time.
We claim that $a_{n_0}-\frac{c}{6}$ and $b_{n_0}+\frac{c}{6}$ have the desired property. It is not difficult to see that both are rational numbers, follows immediately by construction so, we will show that $a_{n_0}-\frac{c}{6}\le y$, $x\le b_{n_0}+\frac{c}{6}$ and $a_{n_0}-\frac{c}{6}>b_{n_0}+\frac{c}{6}$.
We already know that $|y - a_{n_0}|\le c/6$, so $a_{n_0}-c/6\le y \le a_{n_0}+c/6$ as desired. A similar argument shows that $x\le b_{n_0}+c/6$. To conclude the proof our task is to show $b_{n_0}+c/6<a_{n_0}-c/6$. We argue by contradiction, suppose $b_{n_0}+c/6\ge a_{n_0}-c/6$ then $c/3\ge a_{n_0}-b_{n_0}$. But since $n_0\ge N$, it follows that $a_{n_0}-b_{n_0}\ge c$ and then $c/3\ge c$ a contradiction.
We define $q$ as the average of $a_{n_0}-\frac{c}{6}$ and $b_{n_0}+\frac{c}{6}$ and we're done.
I would appreciate for any suggestion. Thanks in advance. :)
This should be a comment, but I lack the power (insert Scotty reference).
You have stated that $y - x$ is positive, but no where did you assert $y > x$. Of course, you can do that, without loss of generality, but, if you want to precise, you should. Otherwise, looks fine.
Since I'm writing an answer anyway: If you wanted to simplify the final argument and avoid the proof by contradiction, it isn't hard. You've chosen $n_0$ so that $a_{n_0} - b_{n_0} \geq c$. This means that
$$ b_{n_0} + c \leq a_{n_0}.$$
Subtracting $\frac{c}{2}$ from both sides gives the obvious inequalities:
$$ b_{n_0} + \frac{c}{6} < b_{n_0} + \frac{c}{2} \leq a_{n_0} - \frac{c}{2} < a_{n_0} - \frac{c}{6}. $$
Indeed, this shows that either of $b_{n_0} + c/2$ or $a_{n_0} - c/2$ could be the quantity $q$ you sought in the first place. Anyway, your proof is correct.