theorem Th5: :: POSET_1:5

for P being non empty strict chain-complete Poset
for g1, g2 being monotone Function of P,P st g1 <= g2 holds
sup (iter_min g1) <= sup (iter_min g2)