for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))