theorem Th4: :: WELLSET1:4

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