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)