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