:: deftheorem Def2 defines Abelian RLVECT_1:def 2 :
for IT being addMagma holds
( IT is Abelian iff for v, w being Element of IT holds v + w = w + v );