:: deftheorem Def16 defines co-well_founded REWRITE1:def 16 :
for R being Relation holds
( R is co-well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y & a <> b holds
not [a,b] in R ) ) );