theorem :: LATTAD_1:10

for L being AD_Lattice
for x, y being Element of L holds
( x [= y iff x "/\" y = x ) by Lem232;