for R being Relation holds
( R is well_founded iff R is_well_founded_in field R ) ;