theorem Th36: :: LATTICE3:36

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