theorem :: GROUP_1A:281

for G being addGroup
for a, g being Element of G holds a * g in con_class a by Th80, Th74;