let G be addGroup; :: thesis: for A being Subset of G
for H1 being Subgroup of G st A, carr H1 are_conjugated holds
ex H2 being strict Subgroup of G st the carrier of H2 = A
let A be Subset of G; :: thesis: for H1 being Subgroup of G st A, carr H1 are_conjugated holds
ex H2 being strict Subgroup of G st the carrier of H2 = A
let H1 be Subgroup of G; :: thesis: ( A, carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A )
assume A, carr H1 are_conjugated ; :: thesis: ex H2 being strict Subgroup of G st the carrier of H2 = A
then consider g being Element of G such that
A1: A = (carr H1) * g ;
A = the carrier of (H1 * g) by A1, Def6A;
hence ex H2 being strict Subgroup of G st the carrier of H2 = A ; :: thesis: verum