theorem :: ORDERS_1:15

for X being set
for O being Order of X holds field O = X