:: deftheorem defines is_well_founded_with_minimal_set POSET_2:def 7 :
for X being non empty set
for D being Subset of X
for E being Function of X,X holds
( E is_well_founded_with_minimal_set D iff ex l being Function of X,NAT st
for x being Element of X holds
( ( l . x <= 0 implies x in D ) & ( not x in D implies l . (E . x) < l . x ) ) );