theorem :: ORDERS_1:22

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