theorem Lem36c: :: LATTAD_1:31

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