for R being Relation st R is being_linear-order holds
R linearly_orders field R