let G be addGroup; :: thesis: for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
let H1, H2 be strict Subgroup of G; :: thesis: ( H1,H2 are_conjugated implies H2,H1 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: H2,H1 are_conjugated
H2 = H1 * (- g) by A1, ThB62;
hence H2,H1 are_conjugated ; :: thesis: verum