let G be Group; :: thesis: for H2 being Subgroup of G
for H1 being strict Subgroup of G holds
( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
let H2 be Subgroup of G; :: thesis: for H1 being strict Subgroup of G holds
( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
let H1 be strict Subgroup of G; :: thesis: ( H1,H2 are_conjugated iff carr H1, carr H2 are_conjugated )
thus ( H1,H2 are_conjugated implies carr H1, carr H2 are_conjugated ) :: thesis: ( carr H1, carr H2 are_conjugated implies H1,H2 are_conjugated )

proof

given a being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ a ; :: according to GROUP_3:def 11 :: thesis: carr H1, carr H2 are_conjugated
carr H1 = (carr H2) |^ a by A1, Def6;
hence carr H1, carr H2 are_conjugated by Def9; :: thesis: verum

end;

given a being Element of G such that A2: carr H1 = (carr H2) |^ a ; :: according to GROUP_3:def 9 :: thesis: H1,H2 are_conjugated
H1 = H2 |^ a by A2, Def6;
hence H1,H2 are_conjugated by Def11; :: thesis: verum