theorem LemXX: :: LATTAD_1:5

for L being AD_Lattice
for x, y being Element of L holds (x "/\" y) "\/" y = y