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