let G be Group; :: thesis: for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
let a, b be Element 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 7 :: thesis: b,a are_conjugated
b = a |^ (g " ) by A1, Th30;
hence b,a are_conjugated by Def7; :: thesis: verum