let G be addGroup; :: 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, ThB37;
hence a,b are_conjugated by Th74, ZFMISC_1:3; :: 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, ThB37;
hence {a},{b} are_conjugated by Th88; :: thesis: verum