let G be addGroup; :: 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: addMagma(# the carrier of H1, the addF of H1 #) = H2 * g ; :: according to GROUP_1A:def 39 :: thesis: ( not H2,H3 are_conjugated or H1,H3 are_conjugated )
given h being Element of G such that A2: addMagma(# the carrier of H2, the addF of H2 #) = H3 * h ; :: according to GROUP_1A:def 39 :: thesis: H1,H3 are_conjugated
H1 = H3 * (h + g) by A1, A2, Th60;
hence H1,H3 are_conjugated ; :: thesis: verum