let G be addGroup; :: thesis: for A being Subset of G holds A,A are_conjugated
let A be Subset of G; :: thesis: A,A are_conjugated
take 0_ G ; :: according to GROUP_1A:def 37 :: thesis: A = A * (0_ G)
thus A = A * (0_ G) by ThB52; :: thesis: verum