Property: ordered field

Definition: the field is totally ordered with an order compatible with the ring operations