theorem :: ORDERS_1:20

for R being Relation st R is being_linear-order holds
( R is being_quasi-order & R is being_partial-order ) ;