theorem :: LATTAD_1:2

for L being AD_Lattice
for x, y being Element of L holds
( x "\/" y = x iff x "/\" y = y ) by DefA1, ROBBINS3:def 3;