theorem :: WELLORD1:3

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