let G be Group; :: 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_3:def 9 :: thesis: B,A are_conjugated
B = A |^ (g " ) by A1, Th63;
hence B,A are_conjugated by Def9; :: thesis: verum