:: deftheorem Def3 defines add-associative RLVECT_1:def 3 :
for IT being addMagma holds
( IT is add-associative iff for u, v, w being Element of IT holds (u + v) + w = u + (v + w) );