:: deftheorem Def12 defines fix_func POSET_1:def 12 :
for P being non empty strict chain-complete Poset
for b₂ being Function of (ConPoset (P,P)),P holds
( b₂ = fix_func P iff for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₂ . g = least_fix_point h );