theorem :: WELLSET1:6

for N being set ex R being Relation st
( R is well-ordering & field R = N )