$\sup\{q \in \mathbb{Q} : q > 0,\ q^2 < 2\} = \sqrt{2}$ in $\mathbb{R}$, and no supremum in $\mathbb{Q}$

In $\mathbb{R}$ we have $2 = 1 + 1 > 0$, so [L1] supplies a unique $r \ge 0$ with $r^2 = 2$; and $r \ne 0$ because $r = 0$ would give $r^2 = 0 \ne 2$, so $r > 0$. Write $r =: \sqrt{2}$.

$S$ is nonempty: the rational $1$ satisfies $1 > 0$ and $1^2 = 1 < 2$, so $1 \in S$.

Let $u \in \mathbb{Q}$ be an arbitrary upper bound of $S$ in $\mathbb{Q}$, that is, $q \le u$ for every $q \in S$.

Let $\varepsilon > 0$ in $\mathbb{R}$ be arbitrary.

The rational $2$ is an upper bound of $S$ in $\mathbb{Q}$, so $S$ is bounded above there: for $q \in S$ order preservation gives $\iota(q) > 0$ and $\iota(q)^2 = \iota(q^2) < \iota(2) = 2 < 2 + 2 = 2 \cdot 2 = \iota(2)^2$, whence $\iota(q) < \iota(2)$ by [L2] and $q < 2$ by order reflection.

$r$ is an upper bound of $\iota(S)$ in $\mathbb{R}$: for $q \in S$ order preservation gives $\iota(q) > 0$ and $\iota(q)^2 = \iota(q^2) < \iota(2) = 2 = r^2$, so $\iota(q) < r$ by [L2], hence $\iota(q) \le r$.

$r$ is not the image of any rational: if $r = \iota(q)$ then $\iota(q^2) = \iota(q)^2 = r^2 = 2 = \iota(2)$, so $q^2 = 2$ by injectivity of $\iota$, which [L5] forbids.

Put $a_\varepsilon := \max\{0,\ r - \varepsilon\}$, which exists by [L7]; then $0 \le a_\varepsilon$, and $a_\varepsilon < r$ because $a_\varepsilon$ is one of the two entries $0$ and $r - \varepsilon$, of which the first is $< r$ by 1.1 and the second is $< r$ because $\varepsilon > 0$.

The image $\iota(u)$ of the bound $u$ is an upper bound of $\iota(S)$ in $\mathbb{R}$: for $q \in S$ the inequality $q \le u$ in $\mathbb{Q}$ gives $\iota(q) \le \iota(u)$ by order preservation.

Density applied to $a_\varepsilon < r$ produces a rational $q_\varepsilon$ with $a_\varepsilon < \iota(q_\varepsilon) < r$; then $\iota(q_\varepsilon) > a_\varepsilon \ge 0$ forces $q_\varepsilon > 0$ by order reflection, and $0 \le \iota(q_\varepsilon) < r$ gives $\iota(q_\varepsilon^2) = \iota(q_\varepsilon)^2 < r^2 = 2 = \iota(2)$ by [L2], hence $q_\varepsilon^2 < 2$ in $\mathbb{Q}$; so $q_\varepsilon \in S$ and $r - \varepsilon \le a_\varepsilon < \iota(q_\varepsilon)$.

The set $\iota(S)$ is nonempty and bounded above in $\mathbb{R}$ by $r$, and for every $\varepsilon > 0$ its element $\iota(q_\varepsilon)$ satisfies $r - \varepsilon < \iota(q_\varepsilon)$; the epsilon characterisation therefore gives $\sup \iota(S) = r = \sqrt{2}$.

Since $r$ is the least upper bound of $\iota(S)$ and $\iota(u)$ is an upper bound of it, we get $r \le \iota(u)$; and $r \ne \iota(u)$ by 2.2, so $r < \iota(u)$.

Density applied to $r < \iota(u)$ produces a rational $v$ with $r < \iota(v) < \iota(u)$; every $q \in S$ satisfies $\iota(q) \le r < \iota(v)$, so $q < v$ by order reflection and $v$ is an upper bound of $S$ in $\mathbb{Q}$; and $v < u$, again by order reflection. Hence $u$ is not $\le$ every upper bound of $S$ in $\mathbb{Q}$, so $u$ is not a supremum of $S$ in $\mathbb{Q}$.

The upper bound $u$ was an arbitrary one, so no upper bound of $S$ in $\mathbb{Q}$ is least: $S$ has a supremum in $\mathbb{R}$, equal to $\sqrt{2}$, and has no supremum in $\mathbb{Q}$ even though it is nonempty and bounded above there, for instance by $2$.