theorem Th28: :: WELLORD1:28

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