theorem :: LATTAD_1:33

for L being GAD_Lattice
for x, y being Element of L holds
( (x "/\" y) "\/" x = x iff x "/\" (y "\/" x) = x ) by Th3712;