theorem :: WELLORD1:4

for R being Relation holds
( R well_orders field R iff R is well-ordering )