theorem Th4: :: POSET_1:4

for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))