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