:: deftheorem defines meet-Absorbing ROBBINS3:def 3 :
for L being non empty LattStr holds
( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x );