theorem Th3: :: WELLSET1:3

for x, y being set
for W being Relation st x in field W & y in field W & W is well-ordering & not x in W -Seg y holds
[y,x] in W