let G be Group; :: 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_3:def 9 :: 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