:: deftheorem Def5 defines least_fix_point POSET_1:def 5 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous holds
for b₃ being Element of P holds
( b₃ = least_fix_point g iff ( b₃ is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b₃ <= p ) ) );