for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr
for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x