theorem :: LATWAL_1:6

for L being WA_Lattice
for x, y being Element of L holds
( x "/\" y = x iff x [= y ) by LATTICES:4;