:: deftheorem Def3 defines well_founded WELLFND1:def 3 :
for R being RelStr
for X being Subset of R holds
( X is well_founded iff the InternalRel of R is_well_founded_in X );