theorem :: WELLORD1:7

for R being Relation st R is well-ordering & field R <> {} holds
ex a being object st
( a in field R & ( for b being object st b in field R holds
[a,b] in R ) ) by Th6;