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