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 Lemfixpoint01;
then A2: least_fix_point g <= sup (iter_min g) by Defleastfixpoint;
least_fix_point g is_a_fixpoint_of g by Defleastfixpoint;
then sup (iter_min g) <= least_fix_point g by Lemfixpoint02;
hence least_fix_point g = sup (iter_min g) by A2, ORDERS_2:25; :: thesis: verum