Real closure theorem
= Real closure theorem
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.