for P being non empty strict chain-complete Poset
for g1, g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point g1 <= least_fix_point g2