for L being non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y