\begin{definition}[Definition:Positive/Real Number]
The '''positive real numbers''' are the set:
:$\R_{\ge 0} = \set {x \in \R: x \ge 0}$
That is, all the real numbers that are greater than or equal to zero.
Thus, in Wirth interval notation:
:$\R_{\ge 0} = \hointr 0 \to$
\end{definition}