let G be Group; :: thesis: for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
let a, b be Element of G; :: thesis: ( {a},{b} are_conjugated iff a,b are_conjugated )
thus ( {a},{b} are_conjugated implies a,b are_conjugated ) :: thesis: ( a,b are_conjugated implies {a},{b} are_conjugated )

proof

assume {a},{b} are_conjugated ; :: thesis: a,b are_conjugated
then consider g being Element of G such that
A1: {a} |^ g = {b} by Th104;
{b} = {(a |^ g)} by A1, Th44;
then b = a |^ g by ZFMISC_1:3;
hence a,b are_conjugated by Th88; :: thesis: verum

end;

assume a,b are_conjugated ; :: thesis: {a},{b} are_conjugated
then consider g being Element of G such that
A2: a |^ g = b by Th88;
{b} = {a} |^ g by A2, Th44;
hence {a},{b} are_conjugated by Th104; :: thesis: verum