for L being with_suprema Poset
for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)