theorem Th41: :: LATTICE3:41
for C being complete Lattice
for a being Element of C
for X being set st a in X & a is_less_than X holds
"/\" (X,C) = a