Ordered Field

An ordered field is a field $F$ together with a binary relation $\le$ on $F$ such that $\le$ is a total order on $F$, and the order is compatible with the field operations in the following sense.

1. For all $a,b,c\in F$, if $a\le b$, then $a+c\le b+c$.
2. For all $a,b\in F$, if $0\le a$ and $0\le b$, then $0\le ab$.