let G be Group; :: thesis: for A, B, C being Subset of G st A,B are_conjugated & B,C are_conjugated holds
A,C are_conjugated
let A, B, C be Subset 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 9 :: 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 9 :: thesis: A,C are_conjugated
A = C |^ (h * g) by A1, A2, Th56;
hence A,C are_conjugated by Def9; :: thesis: verum