theorem :: ORDERS_3:2

for R being Relation
for a being set st R is Order of {a} holds
R = id {a}