theorem :: ORDERS_1:23

for X being set
for O being Order of X holds O is being_quasi-order ;