:: deftheorem defines well_founded WELLFND1:def 2 :
for R being RelStr holds
( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R );