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