:: deftheorem defines is_well_founded_in WELLORD1:def 3 :
for R being Relation
for X being set holds
( R is_well_founded_in X iff for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y ) );