theorem :: ORDERS_1:37

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