Real closure ($K^{\mathrm{rc}}$)

A real closure of an ordered field $K$ is a real closed algebraic extension whose order extends the chosen order of $K$. Existence is the real closure theorem; uniqueness holds up to ordered field isomorphism over $K$. A different ordering of a formally real field can produce a different ordered real closure.

Every ordered field has an ordered algebraic real closure. Combined with the Artin-Schreier ordering criterion, every formally real field embeds into a real closed field. This is one embedding direction in the model companion relation between their theories.