for C being complete Lattice
for a being Element of C
for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C)