theorem Lem316: :: LATTAD_1:63

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