for P1, P2 being non empty Poset
for K being non empty Chain of P1
for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2