theorem :: ORDERS_1:44

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