for L being WA_Lattice
for x, y being Element of L ex z being Element of L st
( x [= z & y [= z & ( for u being Element of L st x [= u & y [= u holds
z [= u ) )