for x being set
for G being Group
for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )