let G be Group; :: thesis: for H1 being strict Subgroup of G holds H1,H1 are_conjugated
let H1 be strict Subgroup of G; :: thesis: H1,H1 are_conjugated
take 1_ G ; :: according to GROUP_3:def 11 :: thesis: multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G)
thus multMagma(# the carrier of H1, the multF of H1 #) = H1 |^ (1_ G) by Th61; :: thesis: verum