theorem :: ORDERS_1:16

for R being Relation st R is being_quasi-order holds
R ~ is being_quasi-order ;