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