theorem :: ORDERS_1:43

for X being set
for O being Order of X holds O quasi_orders X