theorem Seventh: :: ROBBINS5:9

for L being non empty LattStr st L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) holds
for v0, v1, v2 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)