theorem Th3: :: ORDERS_1:3

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