theorem Th40: :: LATTICE3:40

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