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