let G be Group; :: thesis: for A being Subset of G holds A,A are_conjugated
let A be Subset of G; :: thesis: A,A are_conjugated
take 1_ G ; :: according to GROUP_3:def 9 :: thesis: A = A |^ (1_ G)
thus A = A |^ (1_ G) by Th52; :: thesis: verum