theorem :: WAYBEL_0:55

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)