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