theorem :: LATWAL_1:16

for L being WA_Lattice
for x, y, z being Element of L st z [= x & z [= y holds
(x "/\" y) "/\" z = x "/\" (y "/\" z)