:: deftheorem defines * GROUP_1A:def 30 :
for G being addGroup
for a, b being Element of G holds a * b = ((- b) + a) + b;