let G be Group; :: thesis: for a, b, c being Element of G st a,b are_conjugated & b,c are_conjugated holds
a,c are_conjugated
let a, b, c be Element of G; :: thesis: ( a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated )
given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def 7 :: thesis: ( not b,c are_conjugated or a,c are_conjugated )
given h being Element of G such that A2: b = c |^ h ; :: according to GROUP_3:def 7 :: thesis: a,c are_conjugated
a = c |^ (h * g) by A1, A2, Th29;
hence a,c are_conjugated by Def7; :: thesis: verum