:: deftheorem defines iter_min POSET_1:def 3 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iter_min g = iterSet (g,(Bottom P));