for L being WA_Lattice
for x, y being Element of L st x [= y & y [= x holds
x = y by LATTICES:8;