let G be addGroup; :: thesis: for A, B being Subset of G st A,B are_conjugated holds
B,A are_conjugated
let A, B be Subset of G; :: thesis: ( A,B are_conjugated implies B,A are_conjugated )
given g being Element of G such that A1: A = B * g ; :: according to GROUP_1A:def 37 :: thesis: B,A are_conjugated
B = A * (- g) by A1, Th54;
hence B,A are_conjugated ; :: thesis: verum