for X being set
for R being Relation st R well_orders X holds
for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )