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