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