let P be non empty strict chain-complete Poset; :: thesis: for g1, g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point g1 <= least_fix_point g2
let g1, g2 be continuous Function of P,P; :: thesis: ( g1 <= g2 implies least_fix_point g1 <= least_fix_point g2 )
assume A1: g1 <= g2 ; :: thesis: least_fix_point g1 <= least_fix_point g2
set p1 = sup (iter_min g1);
set p2 = sup (iter_min g2);
( sup (iter_min g1) = least_fix_point g1 & sup (iter_min g2) = least_fix_point g2 ) by Th9;
hence least_fix_point g1 <= least_fix_point g2 by A1, Th5; :: thesis: verum