let P be non empty strict chain-complete Poset; :: thesis: for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)
let g be continuous Function of P,P; :: thesis: least_fix_point g = sup (iter_min g)
set p = sup (iter_min g);
set q = least_fix_point g;
sup (iter_min g) is_a_fixpoint_of g by Lm8;
then A1: least_fix_point g <= sup (iter_min g) by Def5;
least_fix_point g is_a_fixpoint_of g by Def5;
then sup (iter_min g) <= least_fix_point g by Lm9;
hence least_fix_point g = sup (iter_min g) by A1, ORDERS_2:2; :: thesis: verum