:: deftheorem defines is_well_founded_with_minimal_set POSET_2:def 10 :
for X being non empty set
for D being Subset of X
for E1, E2 being Function of X,X holds
( E1,E2 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 . (E1 . x) < l . x & l . (E2 . x) < l . x ) ) ) );