for L being non empty join-commutative meet-commutative distributive LattStr
for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) by LATTICES:def 11;