:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :
for G being Group
for a, b being Element of G holds
( a,b are_conjugated iff ex g being Element of G st a = b |^ g );