theorem Th1726: :: LATTAD_1:15

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