theorem Th1712: :: LATTAD_1:12

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