let G be addGroup; :: 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 0_ G ; :: according to GROUP_1A:def 39 :: thesis: addMagma(# the carrier of H1, the addF of H1 #) = H1 * (0_ G)
thus addMagma(# the carrier of H1, the addF of H1 #) = H1 * (0_ G) by Th61; :: thesis: verum