for L being sup-Semilattice
for C being non empty Subset of L st ( for x, y being Element of L st x in C & y in C & not x <= y holds
y <= x ) holds
for Y being non empty finite Subset of C holds "\/" (Y,L) in Y