:: deftheorem Def2 defines well_founded WELLORD1:def 2 :
for R being Relation holds
( R is well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y ) );