theorem :: GROUP_1A:2

for S being non empty addMagma st ( for r, s, t being Element of S holds (r + s) + t = r + (s + t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r + t = s & ex t being Element of S st t + r = s ) ) holds
( S is add-associative & S is addGroup-like )