let G be Group; :: thesis: for a being Element of G holds a,a are_conjugated
let a be Element of G; :: thesis: a,a are_conjugated
take 1_ G ; :: according to GROUP_3:def 7 :: thesis: a = a |^ (1_ G)
thus a = a |^ (1_ G) by Th19; :: thesis: verum