theorem Th34: :: LATTICE3:34

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