theorem Th4: :: WAYBEL30:4

for R being Semilattice
for D being non empty directed Subset of (InclPoset (Ids R))
for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }