theorem :: ORDERS_1:12

for X being set
for R being total Relation of X holds field R = X by Lm4;