theorem :: GROUP_1A:283

for G being addGroup
for a, b being Element of G st a in con_class b holds
b in con_class a