theorem :: LATTAD_1:13

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