for L being non empty up-complete Poset
for D being non empty finite directed Subset of L holds sup D in D