let G be addGroup; :: 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_1A:def 37 :: 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 37 :: thesis: A,C are_conjugated
A = C * (h + g) by A1, A2, Th47;
hence A,C are_conjugated ; :: thesis: verum