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