let G be Group; :: thesis: for H3 being Subgroup of G
for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
let H3 be Subgroup of G; :: thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated & H2,H3 are_conjugated holds
H1,H3 are_conjugated
let H1, H2 be strict Subgroup of G; :: thesis: ( H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated )
given g being Element of G such that A1: multMagma(# the carrier of H1,the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def 11 :: thesis: ( not H2,H3 are_conjugated or H1,H3 are_conjugated )
given h being Element of G such that A2: multMagma(# the carrier of H2,the multF of H2 #) = H3 |^ h ; :: according to GROUP_3:def 11 :: thesis: H1,H3 are_conjugated
H1 = H3 |^ (h * g) by A1, A2, Th72;
hence H1,H3 are_conjugated by Def11; :: thesis: verum