let G be addGroup; :: 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: addMagma(# the carrier of H1, the addF of H1 #) = H2 * a ; :: according to GROUP_1A:def 39 :: thesis: carr H1, carr H2 are_conjugated
carr H1 = (carr H2) * a by A1, Def6A;
hence carr H1, carr H2 are_conjugated ; :: thesis: verum

end;

given a being Element of G such that A2: carr H1 = (carr H2) * a ; :: according to GROUP_1A:def 37 :: thesis: H1,H2 are_conjugated
H1 = H2 * a by A2, Def6A;
hence H1,H2 are_conjugated ; :: thesis: verum