Construction of $\sqrt{2}$ I am working on the formal construction of the positive real numbers. I have the positive real number 2 as the set of positive rational numbers less than 2. I have $\sqrt{2}$ as the set of positive rational numbers the squares of which are less than 2. 
Multiplication of positive real numbers x and y is defined as the set of all positive rational numbers $z=a\times b$ such that $a\in x$ and $b\in y$.
Question: Using these constructions, how can I prove that the $\sqrt{2}\times\sqrt{2} = 2$?
Any help -- hints or online references -- would be appreciated.
Restating question: If $x$ is a positive rational number less than 2, how can I prove there 
exists positive rational numbers $a$ and $b$ such that  $a\times a\lt 2$,  $b\times b \lt 2$  and  $x=a\times b$ ? 
 A: You seem to be using a somewhat non-standard definition of cut; but the idea below can be easily adapted to more standard definitions.  
We want to prove that $\sqrt{2}\times \sqrt{2}=2$.  Of course we mean that the product is equal to the cut "$2$" but it would be a nuisance to give that a new name.
The easy part is to show that every element of $\sqrt{2}\times \sqrt{2}$ is in $2$. For if $a$ and $b$ are positive rationals such that $a^2<2$ and $b^2<2$, then $ab<2$.
Next we need to show that every positive rational $r$ in the cut $2$ can be expressed as $ab$, where $a$ and $b$ are positive rationals and $a^2<2$, $b^2<2$.  
The idea is to show that there is a positive rational $b$ such that $r<b^2<2$. Then let $a=r/b$. Certainly $ab=r$. Also, $a^2=r^2/b^2=r(r/b^2)<(2)(1)=2$.
We construct $b$.  There are many ways to do the job. For instance we can use the estimates associated with the usual Newton Method procedure for approximating $\sqrt{2}$. However, we choose to use an argument that is closer in spirit to the continuity proof for $\sqrt{x}$.
Let $\epsilon=\min(2-r, 1)$, and let $n$ be a positive integer such that $10n/n^2<\epsilon$.  There is a perfect square $m^2$ such that $2n^2-10n\le m^2<2n^2$. Let $b=m/n$. Then $r<b^2<2$, and we are done.
