let G be addGroup; :: 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_1A:def 35 :: thesis: b,a are_conjugated
b = a * (- g) by A1, ThB25;
hence b,a are_conjugated ; :: thesis: verum