for G being addGroup st ( for a, b being Element of G holds a * b = a ) holds
G is Abelian