:: deftheorem Def7 defines meet-associative LATTICES:def 7 :
for IT being non empty /\-SemiLattStr holds
( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c );