Algebraic closure of a real-closed field

Question

There is a theorem that says:

$K$ is a real-closed field if and only if (1) $x^2+1$ is irreducible in $K$ and (2) $K(i)$ is algebraically closed (where $i$ is a root of $x^2+1$ in an algebraic closure of $K$).

Question: Is $K(i)$ an algebraic closure of $K$?

Answer 1

If the hypothesis of your theorem are fulfilled, then $K(i)$ is algebraically closed and contains $K$, and hence is an algebraic closure of $K$.