Non-Archimedean real closed field (source code)

= Non-Archimedean real closed field
{c}

A non-Archimedean real closed field contains a positive element larger than every standard integer. Compactness constructs one by adjoining a constant $c$ and the formulas $c>n$ for all natural numbers $n$.