let G be addGroup; for a, b being Element of G holds
( {a},{b} are_conjugated iff a,b are_conjugated )
let a, b be Element of G; ( {a},{b} are_conjugated iff a,b are_conjugated )
thus
( {a},{b} are_conjugated implies a,b are_conjugated )
( a,b are_conjugated implies {a},{b} are_conjugated )
assume
a,b are_conjugated
; {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; verum