for G being Group
for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds
a = 1_ G