theorem :: LATTAD_1:34

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