theorem Th22: :: YELLOW_2:22

for X being set
for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" (X,L) & "/\" (X,L) <= a )