let G be addGroup; :: thesis: for A, B being Subset of G holds
( A,B are_conjugated iff ex g being Element of G st B = A * g )
let A, B be Subset of G; :: thesis: ( A,B are_conjugated iff ex g being Element of G st B = A * g )
thus ( A,B are_conjugated implies ex g being Element of G st B = A * g ) :: thesis: ( ex g being Element of G st B = A * g implies A,B are_conjugated )

proof

given g being Element of G such that A1: A = B * g ; :: according to GROUP_1A:def 37 :: thesis: ex g being Element of G st B = A * g
A * (- g) = B by A1, Th54;
hence ex g being Element of G st B = A * g ; :: thesis: verum

end;

given g being Element of G such that A2: B = A * g ; :: thesis: A,B are_conjugated
A = B * (- g) by A2, Th54;
hence A,B are_conjugated ; :: thesis: verum