theorem :: LATTAD_1:47

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