theorem Th16: :: WAYBEL17:16

for S, T being non empty reflexive antisymmetric RelStr
for D being non empty directed Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)