for T being with_suprema Poset
for D being non empty finite directed Subset of T holds sup D in D