for G being addGroup
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st b = a * g )