theorem Th3716: :: LATTAD_1:37

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