theorem Lem36c: :: LATTAD_1:11

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