theorem Th2: :: POSET_1:2

for P, Q being non empty strict chain-complete Poset
for L being non empty Chain of P
for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)