:: deftheorem defines are_conjugated GROUP_1A:def 37 :
for G being addGroup
for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st A = B * g );