theorem :: ORDERS_1:19

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