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