theorem :: WELLORD1:8

for R being Relation st R is well-ordering holds
for a being object holds
( not a in field R or for b being object st b in field R holds
[b,a] in R or ex b being object st
( b in field R & [a,b] in R & ( for c being object st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )