theorem Ze: :: LATTAD_1:7

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