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