theorem Th39: :: LATTICE3:39

for C being complete Lattice
for a being Element of C
for X being set st a is_less_than X holds
a [= "/\" (X,C)