theorem Th6: :: WAYBEL23:6

for L being lower-bounded sup-Semilattice
for X being Subset of (InclPoset (Ids L)) holds sup X = downarrow (finsups (union X))