theorem Th26: :: WAYBEL_5:26

for L being completely-distributive LATTICE
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)