for G being addGroup
for a being Element of G st ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) holds
a = 0_ G