:: deftheorem defines meet-Associative ROBBINS3:def 2 :
for L being non empty /\-SemiLattStr holds
( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) );