theorem :: LATTAD_1:38

for L being GAD_Lattice
for x, y being Element of L holds
( x [= y iff x "/\" y = x ) by LATTICES:def 9, LATTICES:def 8;