for L being AD_Lattice
for x, y being Element of L holds
( x [= x "\/" y & x "/\" y [= y )