for R being Relation st R is well-ordering holds
for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )