theorem :: ORDERS_1:4

for X, x, y being set
for O being Order of X st x in X & y in X & [x,y] in O & [y,x] in O holds
x = y