theorem Th9: :: WAYBEL13:9

for L being lower-bounded sup-Semilattice
for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X