let G be Group; :: 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: multMagma(# the carrier of H1,the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def 11 :: thesis: H2,H1 are_conjugated
H2 = H1 |^ (g " ) by A1, Th74;
hence H2,H1 are_conjugated by Def11; :: thesis: verum