theorem Th9: :: POSET_1:9

for P being non empty strict chain-complete Poset
for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)