theorem :: LATTICE3:53

for X being set
for D being complete \/-distributive Lattice
for a being Element of D holds
( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) )