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 Th88;
{b} = {(a |^ g)} by A1, Th37;
then b = a |^ g by ZFMISC_1:3;
hence a,b are_conjugated by Th74; :: 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 Th74;
{b} = {a} |^ g by A2, Th37;
hence {a},{b} are_conjugated by Th88; :: thesis: verum